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
>>> 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

Reply via email to