|
From: | Andreas Röhler |
Subject: | Re: Beyond release |
Date: | Mon, 27 Jun 2016 17:33:22 +0200 |
User-agent: | Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.1.0 |
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?
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?
, and because they didn't particularly care about Emacs support — which did cause some frustration in the Isabelle community, btw. 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.
[Prev in Thread] | Current Thread | [Next in Thread] |