[Top][All Lists]

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

Re: Beyond release

From: Phillip Lord
Subject: Re: Beyond release
Date: Mon, 27 Jun 2016 21:35:28 +0100
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.95 (gnu/linux)

Clément Pit--Claudel <address@hidden> writes:

> 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
> protocol.

Ah, didn't know that.

>> 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 :)

Yeah, didn't put that very carefully. I meant "the sort of things that
in the past, we used to do my passing stuff to a REPL and parsing the
results". I.e. not REPL interaction.

> 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.

CIDER uses call-backs, which seems to work okay, and is reasonably easy
to implement with closures.

How much of this could be made generic, I don't know. There are
definately some overlapping issues, though. Asynchronous callbacks are a
little hard to implement and debug, so providing way of making
call-backs that log might be nice.

I'll have a think on it.


reply via email to

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