Re: [isabelle] Isabelle/jedit

On Wed, 25 Jul 2012, Nils Jähnig wrote:

i have this very same problem. especially when "apply auto" follows, but now applies to a different proof state, which it cannot resolve, it takes very long, often too long to wait. the obvious workaround is to comment all those lines, but this is very tedious. right now i usually cut and paste the line oops end (* frequently when i edit larger theory files.

i would also be very happy to see a "parse till cursor"-mode or something in jedit. currently it is "parse the visible lines in the editor" (and lines that were viewed since last edit), but maybe someday Makarius has enough time to include an option to choose (just like the auto update button). maybe auto parse [on/off], and when turned off, you can something like double-click on a line to parse until there.

More refined implicit processing of the editing and checking process is indeed one of the many things that I still need to do, say with timeouts for the part after the main editor focus towards the end of the buffer. But note that the curser as such is somehow an artifact of the TTY with its single-focus model. I would like to overcome that eventually, e.g. to allow looking at several relevant sub-proof states at the same time, while editing the head of an induction proof, say.

In any case it helps to collect observations from users, like on this thread.

One more hint what can be done right now (in Isabelle2012): the main control of the implicit checking is the "perspective" of the editor, i.e. the set of text intervals that are visible to the user. Standard jEdit Folding and Narrowing can be used to confine proof checking to a smaller text region, e.g. via the menu action "Folding / Narrow to Selection".


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