[isabelle-dev] jedit

[Makarius]

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