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
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
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