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). AFAICT, Isabelle moved to jEdit because that's what the authors liked programming in, 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? Clément.