Sounds interesting! Good luck and let us know if we can help again. - D.
On 6 Apr 2012, at 09:04, Edward Z. Yang wrote: > Hello David, > > I'm actually building a domain-specific frontend for Coq, and I didn't > feel like reimplementing all of ProofGeneral's parsing hacks! It's > not much: it's going to be a pedagogical theorem prover for first > order logic, but the idea is to closely support different deduction > styles (e.g. natural deduction, sequent calculus, etc.) > > Thanks, > Edward > > Excerpts from David Aspinall's message of Fri Apr 06 03:49:29 -0400 2012: >> 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 >>> [email protected] >>> 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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
