[isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]
> This is the last chance to report any problems before the official
> release of Isabelle2012.
if, using RC-3 (linux 32 bit), and jedit I edit a new theory, say "test.thy":
lemma shows "True" proof-
And then intend to outcomment the proof attempt by inserting "(*" before the
lemma, and "*)" after the lemma, that is I want to get
(* lemma shows "True" proof- *)
then after inserting the "(*", I get "Outer syntax error:
command expected, but bad input (* was found". Apparently this is
because jedit still assumes that in this scenario I want to be in
prove mode, while of course by outcommenting it I wanted to abandon
the proof attempt. While this is sth I can live with, is it
desired or necessary behavior or sth that ought to be reported?
This archive was generated by a fusion of
Pipermail (Mailman edition) and