Re: Emacs and jEdit

["Andreas Röhler" <andreas.roehler@online.de>]

On 18.07.2016 16:56, Stefan Monnier wrote:
>> 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
>
>

Correction taken WRT protocol, thanks. Being interested to take part 
delivering a new port.

Beside sml-mode.el seems to have some issues. IMO one reason is smie 
introducing complexity.