Re: [isabelle] New error messages in Isabelle 2013

Am 30/01/2013 15:39, schrieb Makarius:
> On Wed, 30 Jan 2013, Lars Noschinski wrote:
>>> I am still confused about this confusion. Taking the above specification
>>> in isolation, it is already what happens in Isabelle2013-RC2: you see
>>> the error "immediately" in the output of the by command, assuming that
>>> window is open in the old-fashioned manner; it also works Proof General.
>>> If you don't have output open, then pointing at the red squiggles of
>>> "auto" gives the error more quickly.
>> I think Peter's point is that he would not like to work with a version of
>> Isabelle where you cannot see directly what is happening at the editing focus.
> When you say "the editing focus" and "directly" it already has a strong bias
> towards the TTY model.  Isabelle/jEdit is moving more and more away from that,
> as far as it becomes feasible.  I am especially interested to see decent Isar
> proof editing facilities, without the TTY side-conditions.

Makarius, your argument is often ideological and not ergonomic. Whenever
somebody mentions anything reminiscent of PG or TTY, it is bad per se for you
and must be abondoned. Unfortunately, some of the points, like an editing focus
and not just "legacy" but have to do something with our cognitive apparatus.
When you are working hard on a particular goal, that is your mental focus, and
you want zero distraction from it. (And you want a quick way to get back to it
when you went somewhere else.)

Here are some distracting features of Isabelle jedit: When I type a proof, the
buffer is constantly reprocessed which leads to a lot of flashing, with red
signs coming on, which makes it harder to think about the problem. When I have
mistyped a formula, it is given a pink background with grey frames around
tokens(?). This makes the formula harder to read and correct (eg the red
squiggle is harder to see). It is a bit like talking to somebody who keeps
interrupting you in the middle of a sentence whenever you pause to breathe. What
I do now is to shut that other person up with the help of one of the macros
provided here
until I am finished thinking and saying what I wanted to say.

Note that my argument is a cognitive one, not based on old vs new. Or, as the
Mizar guys say: Experience, not only doctrine.


> This does not mean that the Output panel of Isabelle/jEdit will just disappear
> in the next release.  There are applications where you do need free-form output
> from commands.
> There are important special cases though:
>   (1) proof development, especially structured proof development
>   (2) feedback from ATPs via sledgehammer etc.
> Here I can imagine more direct user interface support than the old TTY loop.
>     Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.