lib/ProofGeneral/pgml.rnc
author blanchet
Fri Apr 26 12:09:51 2013 +0200 (2013-04-26)
changeset 51790 22517d04d20b
parent 33686 8e33ca8832b1
permissions -rw-r--r--
more intuitive syntax for equality-style discriminators of nullary constructors
     1 # 
     2 # RELAX NG Schema for PGML, the Proof General Markup Language
     3 # 
     4 # Authors:  David Aspinall, LFCS, University of Edinburgh       
     5 #           Christoph Lueth, University of Bremen       
     6 # 
     7 # Status:  Complete, prototype.
     8 # 
     9 # For additional commentary, see accompanying commentary document
    10 # (available at http://proofgeneral.inf.ed.ac.uk/kit)
    11 # 
    12 # Advertised version: 1.0
    13 # 
    14 
    15 pgml_version_attr = attribute version { xsd:NMTOKEN }
    16 
    17 pgml =
    18   element pgml {
    19     pgml_version_attr?,
    20     (statedisplay | termdisplay | information | warning | error)*
    21   }
    22 
    23 termitem      = action | nonactionitem
    24 nonactionitem = term | pgmltype | atom | sym
    25 
    26 pgml_mixed    = text | termitem | statepart 
    27 
    28 pgml_name_attr = attribute name { text }
    29 
    30 kind_attr = attribute kind { text }
    31 systemid_attr = attribute systemid { text }
    32 
    33 statedisplay =
    34   element statedisplay {
    35     pgml_name_attr?, kind_attr?, systemid_attr?,
    36     pgml_mixed*
    37   }
    38 
    39 pgmltext    = element pgmltext { (text | termitem)* }
    40 
    41 information = element information { pgml_name_attr?, kind_attr?, pgmltext }
    42 
    43 warning     = element warning     { pgml_name_attr?, kind_attr?, pgmltext }
    44 error       = element error       { pgml_name_attr?, kind_attr?, pgmltext }
    45 statepart   = element statepart   { pgml_name_attr?, kind_attr?, pgmltext }
    46 termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext }
    47 
    48 pos_attr    = attribute pos { text }
    49 
    50 term        = element term { pos_attr?, kind_attr?, pgmltext }
    51 
    52 # maybe combine this with term and add extra attr to term?
    53 pgmltype    = element type { kind_attr?, pgmltext }
    54 
    55 action      = element action { kind_attr?, (text | nonactionitem)* }
    56 
    57 fullname_attr = attribute fullname { text }
    58 atom = element atom { kind_attr?, fullname_attr?, text }
    59 
    60 
    61 ## Symbols
    62 ##
    63 ## Element sym can be rendered in three alternative ways, 
    64 ## in descending preference order:
    65 ##
    66 ## 1) the PGML symbol given by the name attribute
    67 ## 2) the text content of the SYM element, if non-empty
    68 ## 3) one of the previously configured text alternatives advertised
    69 ##    by the component who produced this output.
    70 ##
    71 symname_attr = attribute name { token }        # names must be [a-zA-Z][a-zA-Z0-9]+
    72 sym          = element sym { symname_attr, text }
    73 
    74 
    75 pgmlconfigure = symconfig              # inform symbol support (I/O) for given sym
    76 
    77 textalt = attribute alt { text }       # text alternative for given sym
    78 
    79 symconfig = element symconfig { symname_attr, textalt* }