1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
#
# RELAX NG Schema for PGML, the Proof General Markup Language
#
# Authors: David Aspinall, LFCS, University of Edinburgh
# Christoph Lueth, University of Bremen
# Version: pgml.rnc,v 1.5 2003/09/23 23:12:47 da Exp
#
# Status: Complete but experimental version.
#
# For additional commentary, see the Proof General Kit white paper,
# available from http://www.proofgeneral.org/kit
#
# Advertised version: 1.0
#
pgml_version_attr = attribute version { xsd:NMTOKEN }
pgml =
element pgml {
pgml_version_attr?,
(statedisplay | termdisplay | information | warning | error)*
}
termitem = action | nonactionitem
nonactionitem = term | pgmltype | atom | sym
pgml_name_attr = attribute name { text }
kind_attr = attribute kind { text }
systemid_attr = attribute systemid { text }
statedisplay =
element statedisplay {
pgml_name_attr?, kind_attr?, systemid_attr?,
(text | termitem | statepart)*
}
pgmltext = (text | termitem)*
information =
element information { pgml_name_attr?, kind_attr?, pgmltext }
warning = element warning { pgml_name_attr?, kind_attr?, pgmltext }
error = element error { pgml_name_attr?, kind_attr?, pgmltext }
statepart = element statepart { pgml_name_attr?, kind_attr?, pgmltext }
termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext }
pos_attr = attribute pos { text }
term = element term { pos_attr?, kind_attr?, pgmltext }
# maybe combine this with term and add extra attr to term?
pgmltype = element type { kind_attr?, pgmltext }
action = element action { kind_attr?, (text | nonactionitem)* }
fullname_attr = attribute fullname { text }
atom = element atom { kind_attr?, fullname_attr?, text }
## Symbols
symname_attr = attribute name { text }
sym = element sym { symname_attr }
# configuring PGML
pgmlconfigure = symconfig # inform symbol support (I/O) for given sym
asciialt = attribute alt { text } # understanding of ASCII alt for given sym
symconfig = element symconfig { symname_attr, asciialt? }
|
