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