Re: [isabelle] Isabelle/jedit
2012/7/23 Tobias Nipkow <nipkow at in.tum.de>
> This brings me to the next issue. Not updating the output panel does not
> the prover from evaluating my partially edited proof text in the
> background. But
> since I have edited the beginning of the text, the rest often does not make
> sense anymore, or the parser parses it in an unintended way, at least up
> to the
> next synchronisation point like "lemma". Frequently this leads to diverging
> proof steps a bit further down, which are shown in purple. Together with
> the fan
> coming on this is a bit distracting and I often feel compelled to comment
> bits of the proof in response. Is there any way to control the over-eager
> evaluation to avoid such situations?
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and