[isabelle-dev] Removing TTY / Proof General support

Makarius makarius at sketis.net
Sun Nov 2 20:07:42 CET 2014

On Sat, 18 Oct 2014, Makarius wrote:

> Back to the canonical question about "remainig uses of Proof General". After 
> talking to many people at VSL 2014 Vienna (July 2014) and in the months 
> afterwards, my conclusion is that nothing is left to hold us back.
> So I am leaving a time window of 1-2 weeks, to put forward reasons to 
> postpone the removal of TTY / Proof General support in Isabelle once more. If 
> nothing happens, I will start dismantling legacy code before the end of 
> October 2014.

This is now Isabelle/22b87ab47d3b, with the following lakonic NEWS entry:

* Proof General support has been discontinued.  Minor INCOMPATIBILITY.

The change is already 2.5 days old, but I got distracted with many small 
follow-up changes: after discontinuation of the TTY mode (98c03412079b) 
suddenly many odd things became loose and could be removed.  More will 
follow ...


                   http://stop-ttip.org  774,909 people so far

More information about the isabelle-dev mailing list