Hello Edward 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 <errorresponse fatality="fatal">. Hope this helps, - David 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? > > Cheers, > Edward > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
