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

-- Paul
ProofGeneral-devel mailing list

Reply via email to