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



On Tue, 22 May 2012, Tobias Nipkow wrote:

(The cut-and-repaste workaround is non-disruptive enough that I am fine with it. If the only workaround I knew would be reloading (and thus reproving and losing Undo and a lot of time), I would probably switch back to Proof General).

I am afraid I was in this situation earlier on and I just gave up on jedit.

I need to recall some Isabelle/jEdit history here: for 4 years or so I've been trying desparately make a future beyond Proof General / Emacs happen. In Isabelle2012 it is now the second stable release of it, after the one of Isabelle2011-1. The quality of the result critically depends on feedback by early adopters, not silently giving things up.

So far I've often had the impression that many peoples don't want to go beyond Proof General at all. This is fine. They only need to organize themselves to maintain Proof General in the future, because I have stopped working on it myself in October 2011. (For the Isabelle2012 release I've invested the canonical 2 weeks of brushing up PG/Emacs into the Windows installer.)

So for me there is no way looking back. I hope to get more constructive feedback on Isabelle/jEdit in the future, and find time to work on the small and big things that still need to be done.


	Makarius





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