[isabelle-dev] Remaining uses of Proof General?

[Makarius]

Some more explanations on the meta-model of this thread:

   * We have about 1 week left on isabelle-dev, to discuss whatever might
     prevent using Isabelle/jEdit smoothly, and why people fall-back on PG
     as a reflex.

   * Then there will be Isabelle2014-RC0, as a published release candidate,
     but *without* forking the Isabelle repository yet.  The same question
     and discussion will continue on isabelle-users, for that version, and
     as anticipation for Isabelle2014.

   * Then there will be VSL 2014 at Vienna, with the Isabelle workshop,
     ITP, UITP and more.  I am myself around 13..18-Jul-2014 (inclusive
     interval).  People can show me things personally, to see where the
     remaining snags are.

   * Then we are heading towards the Isabelle2014 release, with the normal
     Isabelle2014-RC1 and *with* forked repository, shortly after the
     ITP/UITP week of VSL.

     People who are staying themselves longer at VSL and are involved in
     the Isabelle2014 lift-off need to keep this in mind: after the fork
     changes need to be sent to me, not pushed onto the main Isabelle
     repository.

Some time after the release fork, we can look again what the present 
answer to the ultimate question is: Are there remaining uses of Proof 
General, or is Isabelle2014 the last release that supports it? 
(Hopefully not: Is Isabelle2014 the last release ever?)

The Isar TTY loop and its Proof General add-on has become a big burden in 
recent years -- both are essentially legacy.  So it is worth spending 
extra time to deal with this seriously.


 	Makarius