Re: Beyond release

[Phillip Lord]

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.

PHil