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



On Fri, 18 May 2012, Holger Blasum wrote:

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

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).

This is probably an instance of the known incident where the Output panel is not updated automatically as expected. One needs to press the "Update" button manually in such situations.

The coupling of the output window with the cursor movement in the source buffer is sub-optimal in several ways. E.g. it is often unclear to which part of the source text the output actually refers.

This arrangement stems from very early versions of Isabelle/jEdit from about 2-3 years ago.


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.

When you say "workflow" it sounds like such exceptional situations of incremental parsing would occur very often.

Note that it can only happen when you change the "polarity" of quoted material, especially (* ... *) and {* ... *}. The current line is always reparsed fully.

Your original motivation was to abandom a proof attempt temporarily. This can be done formally via the 'oops' command. Comments are relatively rare in formal text anyway, more like % in latex. (Which does not mean that formal text {* ... *} is not subject to the same problem.)


	Makarius





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