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