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
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
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
People who are getting uneasy about too many things changing, could get
active and do some Proof General maintenance instead.
This archive was generated by a fusion of
Pipermail (Mailman edition) and