Re: [isabelle] Isabelle2014 and ProofGeneral
On Sat, 13 Sep 2014, Ian Zimmerman wrote:
I have read that thread now, thanks. I disagree with most of what you
say there, but I can see there's no changing your position, so I will
resist the urge to jump in.
This strange game around Proof General is already quite old. De-facto, I
am the only one who ever invested serious work in its Isabelle
connectivity, and there were many calls to action to continue that by
someone else after the start of PIDE in 2007/2008. Nothing has ever
happened, though. Proof General users are characterised by inactivity.
To disprove that, are you willing to do anything yourself? Today it would
mean doing a few reforms in the Emacs LISP implementation to work directly
with Isabelle process protocol functions, not the obsolete Isar TTY
If there are no hard facts showing up to continue classic Proof General
Isabelle support one more season, it will be removed without further ado
in the next Isabelle release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and