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.

ProofGeneral-devel mailing list

Reply via email to