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.)
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
> > ProofGeneralfirstname.lastname@example.org
> > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
ProofGeneral-devel mailing list