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