[Top][All Lists]

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

Re: Beyond release

From: Clément Pit--Claudel
Subject: Re: Beyond release
Date: Mon, 27 Jun 2016 14:05:31 -0400
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

On 2016-06-27 12:40, Phillip Lord wrote:
> I'm guessing that Isabelle/Emacs integration used "parsing output"
> interaction. FWIW, I think that the days of this form of archictecture
> are numbered. Both scala and clojure interaction now use something with
> a structured protocol, with a specialized server on the scala or clojure
> side. A similar thing is happening with R, also, and maybe with JDEE.

And with Coq, another proof assistant that still uses Emacs as its main IDE. 
We're currently working on porting Proof General to use Coq's structured 

> I don't know if anything could be done, but adding general support for
> repl interaction to core or ELPA would probably be a good thing. I don't
> know if it is possible -- most of the tools that I have mentioned so far
> use different protocols, so perhaps it is not.

Do you really mean REPL interaction? If so, comint-mode does exactly this, I 
think :)
But if you meant structured protocols, then it's tricky; there's indeed a large 
variety of protocols. The main pain point when developing those (based on 
limited experience developing Emacs modes for Dafny, F* and Coq — which all use 
different protocols) is asynchronicity; you end up registering timers to delay 
certain actions or implement queues, and it's pretty tricky to keep the code 
organized properly. 

Attachment: signature.asc
Description: OpenPGP digital signature

reply via email to

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