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



Dear Makarius,

> 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":

	theory test
		imports Main
	begin
	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 

	theory test
		imports Main
	begin
	(* 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?

Best,

-- 
Holger Blasum





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