[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Emacs and jEdit

From: Andreas Röhler
Subject: Re: Emacs and jEdit
Date: Mon, 18 Jul 2016 19:09:38 +0200
User-agent: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.1.0

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.


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.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]