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