Re: [isabelle] New error messages in Isabelle 2013



On Wed, 30 Jan 2013, Tobias Nipkow wrote:

Whenever somebody mentions anything reminiscent of PG or TTY, it is bad per se for you and must be abondoned.

It was David Aspinall and myself who made these things work many years ago, and we knew about the possibilities and technical side-conditions. It was a big thing back then, and definitely not bad. But times are changing, and side-conditions what can be done.

The Isabelle/jEdit document model is not so exotic, it is just Isabelle/Isar transferred into what you see in many maintstream IDEs now, and none of them resembles Emacs or TTY-style proof checking. E.g. see http://www.jetbrains.com/idea/

Isar proofs are not scripts. Even in 1999 they were called documents already, despite Proof General having a "scripting" mode only.


When I started the Prover IDE project some years ago, I made clear from the beginning that it is not going to be a clone of Proof General, but an exploration of what can be done beyond the accidental side-conditions of a certain time.

I pointed out many times, that everyone who is strongly attached to Proof General is welcome to continue its maintenance. I am even ready to give some tips what needs to be done, but nothing has happened since
October 2011.

People who are getting uneasy about too many things changing, could get active and do some Proof General maintenance instead.


	Makarius





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