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



On Fri, 18 May 2012, Holger Blasum wrote:

And then intend to outcomment the proof attempt by inserting "(*" before the lemma, and "*)" after the lemma

then after inserting the "(*", I get "Outer syntax error: command expected, but bad input (* was found".

While this is sth I can live with, is it desired or necessary behavior or sth that ought to be reported?

The behaviour is a consequence how the parser of text changes works, so it is necessary in that sense. It is also officially specified as a feature in the REAME:

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

This does not mean the specification could not be improved. Compared to Isabelle2011-1 it is already slightly better in Isabelle2012, and is anticipated to improve further.


	Makarius





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