[isabelle-dev] Removing TTY / Proof General support

[Makarius]

Dear all,

Isabelle2011-1 (October 2011) was notable as the release of the first 
usable PIDE application: Isabelle/jEdit 1.0 according to retrospective 
version numbering.  3 years have passed since then.

Isabelle2014 (August 2014) already has Isabelle/jEdit at version 5.0, 
which is the comfortable and powerful Prover IDE that we know today.  We 
can be also glad to see some alternative PIDE front-ends emerging, namely 
Clide and Isabelle/Eclipse.

Since the TTY and PG legacy in Isabelle is a significant burden on the 
system architecture, I have started to think about the conseqences of its 
removal this spring/summer.  Quite some old rubble will get out of the 
way, once that is disentangled and garbage-collected from the code base; 
important reforms will have a better chance to get through eventually.


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.


 	Makarius

----------------------------------------------------------------------------
                               http://stop-ttip.org
----------------------------------------------------------------------------