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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and