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