Dear Proof General developers,
we are presently in the phase of testing release candidates for
Isabelle2015, which is scheduled for the end of May (or start of June)
2015. See also http://sketis.net/2015/release-candidates-for-isabelle2015
One notable item in the NEWS for this release:
* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
I did this already shortly after the release of Isabelle2014, which is the
last Isabelle release with Proof General and TTY loop support. See also
http://sketis.net/2014/discontinuation-of-isabelle-proof-general
The removal of TTY interaction was a great relieve to the Isabelle system
implementation, and opened up many opportunities for reforms that were
unthinkable before.
Since Isabelle no longer works with Proof General, you may consider
liberating the Proof General code base from the corresponding modules, and
thus maybe move forward as well.
An alternative scenario was sketched on the above blog entry in
15-Nov-2014:
It should be noted that the general PIDE protocol infrastructure is
sufficiently flexibile to support old-fashioned stepping through proof
scripts as well, maybe even with some Emacs front-end. So Proof General
veterans who do care enough about that may assemble at the
proofgeneral-devel mailing list to prove that this old warrior is
not-quite-dead yet.
While it is technically feasible to connect Proof General to
Isabelle/Scala/PIDE in some imitation of the old TTY mode, I personally
don't believe that there are serious adherents to Emacs still around to do
that.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
