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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
|
<?xml version="1.0" encoding="UTF-8"?>
<!-- DTD for PGIP, the Proof General Interface Protocol -->
<!-- Author: David Aspinall, LFCS, University of Edinburgh -->
<!-- Version: pgip.dtd,v 1.6 2001/09/10 19:00:42 da Exp -->
<!-- Status: Incomplete. -->
<!-- For commentary, see the Proof General Kit white paper, -->
<!-- available from http://www.proofgeneral.org/kit -->
<!ELEMENT pgip (%provermsg; | %kitmsg;)*>
<!ATTLIST pgip
version CDATA
class CDATA #IMPLIED
origin CDATA
id CDATA>
<!-- STATUS/ERROR MESSAGES -->
<!-- ===================== -->
<!ELEMENT information (#PCDATA)>
<!ATTLIST information
kind CDATA #IMPLIED
location CDATA #IMPLIED>
<!-- kind=message,urgentmessage,display -->
<!ELEMENT error (#PCDATA)>
<!ATTLIST error
kind CDATA #IMPLIED
location CDATA #IMPLIED>
<!-- kind=warning,fatal,interrupt -->
<!ENTITY % proverstatus "information | error">
<!-- CONFIGURATION MESSAGES -->
<!-- ====================== -->
<!ENTITY % kitconfig "usespgml | haspref | prefval | idtable |
addid | delid | menuadd | menudel | guiconfig">
<!-- This is how it should be:
<!ENTITY % pgml SYSTEM "pgml.dtd">
-->
<!-- Types for config settings -->
<!ELEMENT pgipbool EMPTY>
<!ELEMENT pgipint (#PCDATA)>
<!ELEMENT pgipstring (#PCDATA)>
<!ELEMENT pgipchoice (pgipchoiceitem+)>
<!ELEMENT pgipchoiceitem (#PCDATA)>
<!ATTLIST pgipchoiceitem
tag CDATA #IMPLIED>
<!ENTITY % pgiptype "pgipbool | pgipint | pgipstring | pgipchoice">
<!ELEMENT usespgml EMPTY>
<!ATTLIST usespgml
version CDATA #IMPLIED>
<!ELEMENT haspref pgiptype>
<!ATTLIST haspref
default CDATA #IMPLIED
class CDATA #IMPLIED>
<!ELEMENT prefval (#PCDATA)>
<!ATTLIST prefval
name CDATA #IMPLIED>
<!ELEMENT idtable (#PCDATA)>
<!ATTLIST idtable
class CDATA #IMPLIED>
<!ELEMENT addid (#PCDATA)>
<!ATTLIST addid
class CDATA #IMPLIED>
<!ELEMENT delid (#PCDATA)>
<!ATTLIST delid
class CDATA #IMPLIED>
<!ELEMENT menuadd (#PCDATA)>
<!ATTLIST menuadd
path CDATA #IMPLIED
name CDATA #IMPLIED>
<!ELEMENT menudel (#PCDATA)>
<!ATTLIST menudel
path CDATA #IMPLIED
name CDATA #IMPLIED>
<!-- gui configuration -->
<!-- the PCDATA is the icon, base64-encoded -->
<!ELEMENT objtype (#PCDATA)>
<!ATTLIST objtype
name CDATA #REQUIRED>
<!ELEMENT opn (opsrc, optrg, opcmd)>
<!ATTLIST opn
name CDATA #REQUIRED>
<!-- source types as space-separated list; target type is a single type -->
<!ELEMENT opsrc (#PCDATA)>
<!ELEMENT optrg (#PCDATA)>
<!-- the prover command, with a printf "%1"-style substitution of arguments -->
<!ELEMENT opcmd (#PCDATA)>
<!-- proof operations (no target sort) -->
<!ELEMENT proofopn (opsrc, opcmd)>
<!ATTLIST opn
name CDATA #REQUIRED>
<!-- interactive operations-- require some input -->
<!ELEMENT iopn (inputform, opsrc, optrg, opcmd)>
<!ATTLIST iopn
name CDATA #REQUIRED>
<!-- an input form is a list of fields -->
<!ELEMENT inputform (field)+>
<!-- and a field has a type (int, string, bool, choice(c1...cn)) -->
<!-- and a name; under that name, it will be substituted into the command -->
<!-- Ex. field name=number opcmd="rtac %1 %number" -->
<!-- the PCDATA is the prompt for the input field -->
<!ELEMENT field (pgiptype)>
<!ATTLIST field
type CDATA #REQUIRED
name CDATA #REQUIRED>
<!ELEMENT guiconfig (objtype*, opn*, iopn*, proofopn*) >
<!ENTITY % proverconfig "askpgml | askprefs | resetprefs |
setpref | getpref">
<!ELEMENT askpgml EMPTY>
<!ELEMENT askprefs EMPTY>
<!ATTLIST askprefs
class CDATA #IMPLIED>
<!ELEMENT resetprefs EMPTY>
<!ATTLIST resetprefs
class CDATA #IMPLIED>
<!ELEMENT setpref EMPTY>
<!ATTLIST setpref
class CDATA #IMPLIED>
<!ELEMENT getpref EMPTY>
<!ATTLIST getpref
class CDATA #IMPLIED>
<!-- COMMANDS -->
<!-- ======== -->
<!ELEMENT provercmd (#PCDATA)>
<!ELEMENT goalcmd (#PCDATA)>
<!ELEMENT undocmd EMPTY>
<!ELEMENT abortcmd EMPTY>
<!ELEMENT closecmd (#PCDATA)
goalid CDATA #REQUIRED>
<!ELEMENT postponecmd (#PCDATA)
goalid CDATA #REQUIRED
thmname CDATA #REQUIRED>
<!ELEMENT savecmd EMPTY>
<!ATTLIST savecmd
thmname CDATA #REQUIRED>
<!ELEMENT forgetcmd EMPTY>
<!ATTLIST forgetcmd
thmname CDATA #REQUIRED>
<!ELEMENT restorecmd EMPTY>
<!ATTLIST restorecmd
goalid CDATA #REQUIRED>
<!ELEMENT loadfilecmd (#PCDATA)>
<!ELEMENT retractfilecmd (#PCDATA)>
<!ENTITY % command "provercmd | goalcmd | undocmd | savecmd | forgetcmd |
closecmd | quitcmd | postponecmd | restorecmd |
loadfilecmd | retractfilecmd">
<!-- savecmd Finishes a proof and saves a new theorem
closecmd Temporarily closes a proof and saves state with given id
postponecmd As closecmd, but saves a new theorem and
generates a proof obligation
-->
<!-- Roots of PGIP messages -->
<!-- Messages sent to PG Kit components -->
<!ENTITY % kitmsg "%kitconfig | %proverstatus">
<!-- Messages sent to proof assistant (class "pa") -->
<!ENTITY % provermsg "proverconfig">
<!ELEMENT br EMPTY>
|
