Re: [isabelle] New error messages in Isabelle 2013

Hi Makarius,

I have sent this already in a message previous to this one. The question is
I (as many other Isabelle users, I suppose) depend very much on the output
window to work with
Isabelle even though I work essentially with Isar structured proofs. The
feature is nice, but the output window is better and faster.

The problem is that, in case of a problem in establishing a fact or a
pending goal,
the  output window is now displaying messages
that show both success and failure (jedit-proof-failure) of applying a
given proof method , and
I think this should be avoided at all costs. If it is not possible in
Isabelle 2013, then maybe in Isabelle
2014. In the case of the error message, the output window should display
the message that appear in the image hover-error message, and not an
ambiguous message as
shown  in the jedit-proof-failure image. See attachments.


On Mon, Jan 28, 2013 at 12:42 PM, Makarius <makarius at> wrote:

> On Fri, 25 Jan 2013, Alfio Martini wrote:
>  Instead it is now possible to do quite a lot of proofs right there in the
>>> text, without peeking at the goal state.  You just hover over the red
>>> squiggles of the failed proof methods and immediately see what happened.
>>>  This is escpecially relevant for structured Isar proofs.
>> This is great. I did not know that. I am probably being very naive here
>> (to
>> put it mildly), but what appears in the
>> window that pops up when you hover over the red squiggles is what I would
>> expect to appear
>> in the output window as well (see image attached) .
> The screenshot does not show the position of the cursor (or "caret" in
> Java terminology).  Where is it actually?  The output window follows that,
> in reminiscence of old-style TTY interaction where you have a single focus.
>         Makarius

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: jedit-proof-failure.PNG
Description: PNG image

Attachment: hover-error-message.PNG
Description: PNG image

Attachment: jedit-proof-sucess.PNG
Description: PNG image

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