On Tue, 18 Sep 2012, Tobias Nipkow wrote:
When using jedit (development version) I got into the following situation:
partial proof
(* long
comment
*)
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
summer.
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
distribution.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
