lib/ProofGeneral/pgml.rnc
author wenzelm
Tue, 21 Nov 2006 18:07:33 +0100
changeset 21437 a3c55b85cf0e
parent 17736 863cdca5c77a
child 33686 8e33ca8832b1
permissions -rw-r--r--
moved theorem kinds from PureThy to Thm;
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
# Version: $Id$    
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
     7
# 
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
     8
# Status:  Complete, prototype.
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
     9
# 
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    10
# For additional commentary, see accompanying commentary document
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    11
# (available at http://proofgeneral.inf.ed.ac.uk/kit)
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    12
# 
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    13
# Advertised version: 1.0
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
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    16
pgml_version_attr = attribute version { xsd:NMTOKEN }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    17
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    18
pgml =
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    19
  element pgml {
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    20
    pgml_version_attr?,
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    21
    (statedisplay | termdisplay | information | warning | error)*
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
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    24
termitem      = action | nonactionitem
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    25
nonactionitem = term | pgmltype | atom | sym
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    26
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    27
pgml_mixed    = text | termitem | statepart 
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    28
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    29
pgml_name_attr = attribute name { text }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    30
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    31
kind_attr = attribute kind { text }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    32
systemid_attr = attribute systemid { text }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    33
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    34
statedisplay =
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    35
  element statedisplay {
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    36
    pgml_name_attr?, kind_attr?, systemid_attr?,
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    37
    pgml_mixed*
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
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    40
pgmltext    = element pgmltext { (text | termitem)* }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    41
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    42
information = element information { pgml_name_attr?, kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    43
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    44
warning     = element warning     { pgml_name_attr?, kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    45
error       = element error       { pgml_name_attr?, kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    46
statepart   = element statepart   { pgml_name_attr?, kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    47
termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    48
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    49
pos_attr    = attribute pos { text }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    50
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    51
term        = element term { pos_attr?, kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    52
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    53
# 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
    54
pgmltype    = element type { kind_attr?, pgmltext }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    55
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    56
action      = element action { kind_attr?, (text | nonactionitem)* }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    57
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    58
fullname_attr = attribute fullname { text }
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    59
atom = element atom { kind_attr?, fullname_attr?, text }
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
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    62
## Symbols
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    63
##
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    64
## Element sym can be rendered in three alternative ways, 
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    65
## in descending preference order:
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    66
##
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    67
## 1) the PGML symbol given by the name attribute
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    68
## 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
    69
## 3) one of the previously configured text alternatives advertised
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    70
##    by the component who produced this output.
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    71
##
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    72
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
    73
sym          = element sym { symname_attr, text }
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
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    76
pgmlconfigure = symconfig              # inform symbol support (I/O) for given sym
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    77
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    78
textalt = attribute alt { text }       # text alternative for given sym
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    79
863cdca5c77a Schema files (for information, and validating pgip_isar.xml)
aspinall
parents:
diff changeset
    80
symconfig = element symconfig { symname_attr, textalt* }