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.

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