On 2016-06-27 11:33, Andreas Röhler wrote:
> On 27.06.2016 16:18, Clément Pit--Claudel wrote:
>> On 2016-06-27 05:58, Andreas Röhler wrote:
>>> To make clear, that's not just a personal view, please consider
>>> the withdraw of advanced and promising theorem prover
>>> Isabelle/HOL, which doesn't longer support Emacs, while relying
>>> on it before. BTW that withdraw was in time, before John took
>>> over and AFAIU caused by a policy, which hopefully is abandoned
>>> now.
>> I think that's an incorrect characterisation (see statements that
>> Makarius made on the Proof General mailing list).
> 
> That's where my conclusions are from. Any precise spot to tell
> otherwise?

Yes: Makarius wrote: "While it is technically feasible to connect Proof General to Isabelle/Scala/PIDE in some imitation of the old TTY mode, I personally don't believe that there are serious adherents to Emacs still around to do that."

>> AFAICT, Isabelle moved to jEdit because that's what the authors
>> liked programming in
> 
> That's interesting. Maybe that would also worth being reflected. So
> extending in Java should be easier than in Emacs Lisp? How could it
> came to this?

Does Makarius know Emacs Lisp?

>> What elements make you think Emacs policies had anything to do with
>> it?
> 
> There are several. Think alone the matter of slowness, mentioned
> again and again in bug-reports and development. AFAIU these slowness
> is caused by bugs and design flaws, not by Emacs Lisp as such. The
> introduction of circular dependencies WRT syntax-ppss probably
> deserves being mentioned in this context. Propertize functions are
> encouraged to call syntax-ppss while syntax-ppss itself propertizes.

Interesting. I don't know about these things, but I never saw them them mentioned (especially the last ones) outside of emacs-devel.