For this one I'm not sure if we finalised a markup form that distinguished the 
different semantic parts of proofstate output, although it was certainly 
discussed and seems useful.  The Eclipse interface uses an xslt style sheet to 
render to an HTML widget, so you could add your own tags and interpret them as 
you like.    

I would be tempted to duplicate the names of the hypotheses in attributes, <hyp 
name="Hyp0">...</hyp>, so they are there for the interface to manipulate. 

 - David 

On 6 Apr 2012, at 08:29, Edward Z. Yang wrote:

> In sort of the same vein, in Coq, we have named hypotheses in our
> proof contexts which render like:
>  Hyp0 : Hyp (P x)
>  Hyp1 : Hyp (P z)
>  ============================
>   or (P x) (or (forall y : U, P y) False)
> I'd like to add some PGML so that it looks something like this:
>  <proofstate>
>    <hypotheses>
>      <hyp>Hyp0 : Hyp (P x)</hyp>
>      <hyp>Hyp1 : Hyp (P z)</hyp>
>    </hypotheses>
>    <goal>
>      or (P x) (or (forall y : U, P y) False)
>    </goal>
>  </proofstate>
> But I don't know what the right PGIP/PGML tags are.
> Edward
> Excerpts from Edward Z. Yang's message of Thu Apr 05 23:15:50 -0400 2012:
>> 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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

ProofGeneral-devel mailing list

Reply via email to