Interesting that you're trying this! Although I should warn that we haven't
been actively developing the PGIP infrastructure for a while: which interface
are you hoping to use it with?
Anyway, you should have no problem with multiple <errorresponse> in PGIP. You
need to set the fatality attribute to "warning" (or anything except
"fatal"/"panic"). The restriction you mention applies to the plain text
protocol used inside Emacs for real errors, which correspond to PGIP
Hope this helps,
On 6 Apr 2012, at 04:15, Edward Z. Yang wrote:
> Hello all,
> I'm working on partial PGIP support Coq, and one thing that I would like
> to support is the case when Coq outputs "warning" messages, of which
> there are many but which are nonfatal. I'm wondering what the right
> tag for these are. <errorresponse> is not correct, because we're only
> allowed to have one before <ready/>. Is <metainforesponse> correct?
> It seems too generic, and where am I supposed to attach other metadata?
> ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
ProofGeneral-devel mailing list