Re: Emacs and jEdit

[Stefan Monnier]

> It was supported inside proof-general. But support was withdrawn from
> Isabelle/HOL's side, going frustrated by ongoing difficulties IIUC.

Huh?  Isabelle/HOL developed a fancier protocol/interface for its
various IDEs.  Noone was interested in updating the Emacs-side support
(within Proof-General) to use this new protocol (it required
a significant rewrite because the new protocol works completely
differently).  Then Isabelle/HOL decided to drop support for the old
protocol (at that point only used for Emacs, and the lack of interest in
adapting Emacs's support to the new protocol being taken as a sign that
there weren't enough Emacs users to bother maintaining support for the
old protocol inside Isabelle/HOL).

I can't see any "ongoing difficulties" there.

FWIW, Coq has introduced similarly fancier protocols and since there are
more Emacs+Coq users, some people have taken on the task of updating
Emacs's support (in Proof-General) to use that new protocol (still
ongoing work, AFAIK).  And that work might actually prove useful to
re-introduce Isabelle/HOL support in there, tho that will depend on
whether there's enough motivation for someone to do that part of
the work.


        Stefan