Re: [isabelle] New error messages in Isabelle 2013



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






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