Re: [isabelle] New error messages in Isabelle 2013



On Wed, 30 Jan 2013, René Neumann wrote:

Please keep in mind, that the good ol' TTY approach with only one single
point of focus is not overall obsolete: When dealing with a single
proof, one normally only focuses on the lines one is writing.

This is even before Proof General and especially before Isar proofs. Can you show some of your proofs that you normally do?

I find it very awkward to produce structured proofs with that "good ol'" TTY model, or the slight variation of it in Proof General. Isabelle/jEdit of Isabelle2013 is moving a tiny little bit forward, but still not there to edit proof structure directly, without funny machine state inspection all the time.

But having to use the mouse to get the information is not (even a hotkey for "get message under cursor" probably will be cumbersome).

So maybe that is a starting point to get active, and investigate possibilities of the jEdit platform.

Of course, one would also have to step back, and look conceptually on the problem what the message under the cursor means, bacause that is not fully trivial without assuming an understanding of old-style TTY command boundaries.

Or did you mean a keyboard version of "hover over squiggles"?


	Makarius


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