blob: fbdd9f7d5c739550af50b5ea8a72b3b1d5abcbad (
plain)
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
<?xml encoding="UTF-8"?>
<!--
RELAX NG Schema for PGML, the Proof General Markup Language
Authors: David Aspinall, LFCS, University of Edinburgh
Christoph Lueth, University of Bremen
Version: pgml.dtd,v 1.12 2003/09/23 23:17:18 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
-->
<!ENTITY % pgml_version_attr "
version NMTOKEN #REQUIRED">
<!ELEMENT pgml (statedisplay|termdisplay|information|warning|error)*>
<!ATTLIST pgml
version NMTOKEN #IMPLIED>
<!ENTITY % nonactionitem "term|type|atom|sym">
<!ENTITY % termitem "action|%nonactionitem;">
<!ENTITY % pgml_name_attr "
name CDATA #REQUIRED">
<!ENTITY % kind_attr "
kind CDATA #REQUIRED">
<!ENTITY % systemid_attr "
systemid CDATA #REQUIRED">
<!ELEMENT statedisplay (#PCDATA|%termitem;|statepart)*>
<!ATTLIST statedisplay
name CDATA #IMPLIED
kind CDATA #IMPLIED
systemid CDATA #IMPLIED>
<!ENTITY % pgmltext "(#PCDATA|%termitem;)*">
<!ELEMENT information %pgmltext;>
<!ATTLIST information
name CDATA #IMPLIED
kind CDATA #IMPLIED>
<!ELEMENT warning %pgmltext;>
<!ATTLIST warning
name CDATA #IMPLIED
kind CDATA #IMPLIED>
<!ELEMENT error %pgmltext;>
<!ATTLIST error
name CDATA #IMPLIED
kind CDATA #IMPLIED>
<!ELEMENT statepart %pgmltext;>
<!ATTLIST statepart
name CDATA #IMPLIED
kind CDATA #IMPLIED>
<!ELEMENT termdisplay %pgmltext;>
<!ATTLIST termdisplay
name CDATA #IMPLIED
kind CDATA #IMPLIED>
<!ENTITY % pos_attr "
pos CDATA #REQUIRED">
<!ELEMENT term %pgmltext;>
<!ATTLIST term
pos CDATA #IMPLIED
kind CDATA #IMPLIED>
<!-- maybe combine this with term and add extra attr to term? -->
<!ELEMENT type %pgmltext;>
<!ATTLIST type
kind CDATA #IMPLIED>
<!ELEMENT action (#PCDATA|%nonactionitem;)*>
<!ATTLIST action
kind CDATA #IMPLIED>
<!ENTITY % fullname_attr "
fullname CDATA #REQUIRED">
<!ELEMENT atom (#PCDATA)>
<!ATTLIST atom
kind CDATA #IMPLIED
fullname CDATA #IMPLIED>
<!ENTITY % symname_attr "
name CDATA #REQUIRED">
<!ELEMENT sym EMPTY>
<!ATTLIST sym
%symname_attr;>
<!-- configuring PGML -->
<!ENTITY % pgmlconfigure "symconfig">
<!-- inform symbol support (I/O) for given sym -->
<!ENTITY % asciialt "
alt CDATA #REQUIRED">
<!-- understanding of ASCII alt for given sym -->
<!ELEMENT symconfig EMPTY>
<!ATTLIST symconfig
%symname_attr;
alt CDATA #IMPLIED>
|
