On Sat, Jun 11, 2016 at 3:59 PM, Clément Pit--Claudel <[email protected]> wrote: >> If coqtop works with s-expressions, is the ability to use XML >> maintained? If so, then CoqIDE can still work as it does. If not, >> then CoqIDE is orphaned, yes? Maybe not a great idea to have coqtop >> support two separate protocols. > > Emilio's S-Expressions are built on top of Enrico's Stm, so it isn't really > two separate parts. Additionally, Emilio's protocol comes as a plugin.
OK, a bit clunky, but workable. >> Or are you suggesting that CoqIDE switch to using s-expressions, >> also? > > Emilio is working on that, IIUC. Does he sleep? :-) >> One decision here is whether to use coqtop's -emacs prompt, or the >> vanilla prompt. If we could dump the -emacs prompt, that's another >> desirable (if small) simplification. > > Wouldn't that go away from PG anyway? Since PG would only support the XML or > SEXP protocol. Yes, it would disappear from PG. Maybe there's some advantage of preserving on the coqtop side for the shim (it makes it obvious when you've got a prompt), but maybe that doesn't justify the extra baggage. -- Paul _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
