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
Or did you mean a keyboard version of "hover over squiggles"?
This archive was generated by a fusion of
Pipermail (Mailman edition) and