makarius at sketis.net
Sat Sep 22 20:49:54 CEST 2012
On Tue, 18 Sep 2012, Tobias Nipkow wrote:
> When using jedit (development version) I got into the following situation:
> partial proof
> (* long
> Because of the length of the comment (which was a lemma I had to comment
> out because due to the partial proof above, proof methods in it
> diverged) the end of the comment was outside the window. Now every time
> I would extend the partial proof, I would get "malformed command syntax"
> and had to scroll down to the end of the comment to make that go away.
You have probably noticed that quite a lot has changed here over the
I have now tuned the partial comment behaviour again in
Isabelle/68796a77c42b. There is an option editor_reparse_limit that is
10000 by default, and can be changed in the dialog "Plugins / Plugin
Options / Isabelle / General".
It should be also possible to use the jEdit action "Edit / Source / Range
Comment" to comment out selected areas robustly, although it seems that
jEdit does not re-tokenize the result if it happens to cross the visible
boundary. It should be correct for the document model nonetheless.
The TextTools plugin has a more robust action "Toggle Range Comment".
Maybe I shall map that to the standard key C-e C-c in the Isabelle/jEdit
More information about the isabelle-dev