On Tue, 21 Apr 2015, Stefan Monnier wrote:
don't believe that there are serious adherents to Emacs still around to
Hmm...
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.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
