On Sat, Jun 11, 2016 at 3:59 PM, Clément Pit--Claudel
<clement....@gmail.com> 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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to