lib/ProofGeneral/pgml.rnc
changeset 17736 863cdca5c77a
child 33686 8e33ca8832b1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/ProofGeneral/pgml.rnc	Fri Sep 30 17:28:04 2005 +0200
     1.3 @@ -0,0 +1,80 @@
     1.4 +# 
     1.5 +# RELAX NG Schema for PGML, the Proof General Markup Language
     1.6 +# 
     1.7 +# Authors:  David Aspinall, LFCS, University of Edinburgh       
     1.8 +#           Christoph Lueth, University of Bremen       
     1.9 +# Version: $Id$    
    1.10 +# 
    1.11 +# Status:  Complete, prototype.
    1.12 +# 
    1.13 +# For additional commentary, see accompanying commentary document
    1.14 +# (available at http://proofgeneral.inf.ed.ac.uk/kit)
    1.15 +# 
    1.16 +# Advertised version: 1.0
    1.17 +# 
    1.18 +
    1.19 +pgml_version_attr = attribute version { xsd:NMTOKEN }
    1.20 +
    1.21 +pgml =
    1.22 +  element pgml {
    1.23 +    pgml_version_attr?,
    1.24 +    (statedisplay | termdisplay | information | warning | error)*
    1.25 +  }
    1.26 +
    1.27 +termitem      = action | nonactionitem
    1.28 +nonactionitem = term | pgmltype | atom | sym
    1.29 +
    1.30 +pgml_mixed    = text | termitem | statepart 
    1.31 +
    1.32 +pgml_name_attr = attribute name { text }
    1.33 +
    1.34 +kind_attr = attribute kind { text }
    1.35 +systemid_attr = attribute systemid { text }
    1.36 +
    1.37 +statedisplay =
    1.38 +  element statedisplay {
    1.39 +    pgml_name_attr?, kind_attr?, systemid_attr?,
    1.40 +    pgml_mixed*
    1.41 +  }
    1.42 +
    1.43 +pgmltext    = element pgmltext { (text | termitem)* }
    1.44 +
    1.45 +information = element information { pgml_name_attr?, kind_attr?, pgmltext }
    1.46 +
    1.47 +warning     = element warning     { pgml_name_attr?, kind_attr?, pgmltext }
    1.48 +error       = element error       { pgml_name_attr?, kind_attr?, pgmltext }
    1.49 +statepart   = element statepart   { pgml_name_attr?, kind_attr?, pgmltext }
    1.50 +termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext }
    1.51 +
    1.52 +pos_attr    = attribute pos { text }
    1.53 +
    1.54 +term        = element term { pos_attr?, kind_attr?, pgmltext }
    1.55 +
    1.56 +# maybe combine this with term and add extra attr to term?
    1.57 +pgmltype    = element type { kind_attr?, pgmltext }
    1.58 +
    1.59 +action      = element action { kind_attr?, (text | nonactionitem)* }
    1.60 +
    1.61 +fullname_attr = attribute fullname { text }
    1.62 +atom = element atom { kind_attr?, fullname_attr?, text }
    1.63 +
    1.64 +
    1.65 +## Symbols
    1.66 +##
    1.67 +## Element sym can be rendered in three alternative ways, 
    1.68 +## in descending preference order:
    1.69 +##
    1.70 +## 1) the PGML symbol given by the name attribute
    1.71 +## 2) the text content of the SYM element, if non-empty
    1.72 +## 3) one of the previously configured text alternatives advertised
    1.73 +##    by the component who produced this output.
    1.74 +##
    1.75 +symname_attr = attribute name { token }        # names must be [a-zA-Z][a-zA-Z0-9]+
    1.76 +sym          = element sym { symname_attr, text }
    1.77 +
    1.78 +
    1.79 +pgmlconfigure = symconfig              # inform symbol support (I/O) for given sym
    1.80 +
    1.81 +textalt = attribute alt { text }       # text alternative for given sym
    1.82 +
    1.83 +symconfig = element symconfig { symname_attr, textalt* }