On Tue, 21 Apr 2015, Stefan Monnier wrote:

don't believe that there are serious adherents to Emacs still around to


Maybe I should add the sentence that I deleted before posting the above: I keep telling this story for several years already, and nothing has ever happened from the side of remaining Emacs people. So until there is a constructive proof of serious Emacs development activity, I won't believe it anymore. (The yound and fresh forces have mostly gone over to the vi side.)

It should be actually easier to implement a Proof General backend for current Isabelle/Scala technology, than for the old TTY loop that was removed. It won't give proper PIDE editing, though, just an imitation of the old approach.

The "new" approach (since at least 2009) is direct proof document editing, with continuous feedback from the prover. To digest the prover markup, the editor needs to be quite capable, and single-threaded Emacs probably won't do it.

It would be actually interesting to explore a slightly different approach, where the editor can be weak (Emacs or some HTML front-end). Then the voluminous PIDE document markup is managed by some Scala service in the background, and the editor merely asks for small parts in some kind of "display protocol". The latter notion is by David Aspinall from PGIP, more than 10 years ago.

ProofGeneral-devel mailing list

Reply via email to