On Tue, 21 Apr 2015, Andreas Röhler wrote:
for the sake of a very, very interesting project as Isabelle certainly
looks like, also having done fairly enough mistakes by myself, please
permit to outline what's wrong here IMHO:
first, there is no need to support Emacs actively by any core developers
of a programming language.
Isabelle is not just a programming environment, but primarily for proofs
and proof tools. This poses special challenges to the editing environment
(the IDE) that are addressed by PIDE to a reasonable extent.
Just keep the path open.
The path to connect Emacs to the PIDE infrastructure of Isabelle is still
open. It should be even easier now than the classic Proof General TTY
loop (which I did together with David Aspinall in 1998/1999). It did not
happen so far, and I don't believe it will happen in the foreseeable
future, due to the structure of the remaining Emacs community.
Makarius_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
