Re: [isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]

>   Incremental reparsing sometimes produces unexpected command spans.
>   Workaround: Cut/paste larger parts or reload buffer.

Ok, thanks, works. For the record:

If the cursor *is not* at the end of the theory text
(1) cutting out the entire freshly out-commented section, in our 
case "(* lemma shows "True" proof- *)", 
(2) then repasting it 
==> Exits proof mode and also clears the output window.

If the cursor *is* at the end of the theory text
Doing (1) and (2) above, 
==> Again, exits proof mode. 
In this case, in the "Output" window the syntax error 
message persists, but I can simply ignore it and just type 
on until the system overwrites the output buffer either by a new 
error message or by an empty string (e.g. after accepting a 
successful declaration).

Of course, as the README mentions, there is also the option of 
"File -> Reload", but it involves saving and for me feels more 
disruptive to workflow.


Holger Blasum

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.