author | aspinall |
Sat, 03 Mar 2007 12:42:39 +0100 | |
changeset 22406 | a591df440b5b |
parent 22161 | b2117f4f2d39 |
child 23436 | 343e84195e2c |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/pgip_input.ML |
2 |
ID: $Id$ |
|
3 |
Author: David Aspinall |
|
4 |
||
21940 | 5 |
PGIP abstraction: input commands. |
21637 | 6 |
*) |
7 |
||
8 |
signature PGIPINPUT = |
|
9 |
sig |
|
10 |
(* These are the PGIP commands to which we respond. *) |
|
11 |
datatype pgipinput = |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
12 |
(* protocol/prover config *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
13 |
Askpgip of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
14 |
| Askpgml of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
15 |
| Askconfig of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
16 |
| Askprefs of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
17 |
| Setpref of { name:string, prefcategory:string option, value:string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
18 |
| Getpref of { name:string, prefcategory:string option } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
19 |
(* prover control *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
20 |
| Proverinit of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
21 |
| Proverexit of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
22 |
| Startquiet of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
23 |
| Stopquiet of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
24 |
| Pgmlsymbolson of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
25 |
| Pgmlsymbolsoff of { } |
22406
a591df440b5b
Add setproverflag, to replace other flag controls
aspinall
parents:
22161
diff
changeset
|
26 |
| Setproverflag of { flagname:string, value: bool } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
27 |
(* improper proof commands: control proof state *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
28 |
| Dostep of { text: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
29 |
| Undostep of { times: int } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
30 |
| Redostep of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
31 |
| Abortgoal of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
32 |
| Forget of { thyname: string option, name: string option, |
21867 | 33 |
objtype: PgipTypes.objtype option } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
34 |
| Restoregoal of { thmname : string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
35 |
(* context inspection commands *) |
21867 | 36 |
| Askids of { url: PgipTypes.pgipurl option, |
37 |
thyname: PgipTypes.objname option, |
|
38 |
objtype: PgipTypes.objtype option } |
|
22161 | 39 |
| Askrefs of { url: PgipTypes.pgipurl option, |
40 |
thyname: PgipTypes.objname option, |
|
41 |
objtype: PgipTypes.objtype option, |
|
42 |
name: PgipTypes.objname option } |
|
21867 | 43 |
| Showid of { thyname: PgipTypes.objname option, |
44 |
objtype: PgipTypes.objtype, |
|
45 |
name: PgipTypes.objname } |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
46 |
| Askguise of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
47 |
| Parsescript of { text: string, location: PgipTypes.location, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
48 |
systemdata: string option } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
49 |
| Showproofstate of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
50 |
| Showctxt of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
51 |
| Searchtheorems of { arg: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
52 |
| Setlinewidth of { width: int } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
53 |
| Viewdoc of { arg: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
54 |
(* improper theory-level commands *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
55 |
| Doitem of { text: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
56 |
| Undoitem of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
57 |
| Redoitem of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
58 |
| Aborttheory of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
59 |
| Retracttheory of { thyname: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
60 |
| Loadfile of { url: PgipTypes.pgipurl } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
61 |
| Openfile of { url: PgipTypes.pgipurl } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
62 |
| Closefile of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
63 |
| Abortfile of { } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
64 |
| Retractfile of { url: PgipTypes.pgipurl } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
65 |
| Changecwd of { url: PgipTypes.pgipurl } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
66 |
| Systemcmd of { arg: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
67 |
(* unofficial escape command for debugging *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
68 |
| Quitpgip of { } |
21637 | 69 |
|
70 |
val input : XML.element -> pgipinput option (* raises PGIP *) |
|
71 |
end |
|
72 |
||
73 |
structure PgipInput : PGIPINPUT = |
|
74 |
struct |
|
75 |
||
76 |
open PgipTypes |
|
77 |
||
78 |
(*** PGIP input ***) |
|
79 |
||
80 |
datatype pgipinput = |
|
81 |
(* protocol/prover config *) |
|
82 |
Askpgip of { } |
|
83 |
| Askpgml of { } |
|
84 |
| Askconfig of { } |
|
85 |
| Askprefs of { } |
|
86 |
| Setpref of { name:string, prefcategory:string option, value:string } |
|
87 |
| Getpref of { name:string, prefcategory:string option } |
|
88 |
(* prover control *) |
|
89 |
| Proverinit of { } |
|
90 |
| Proverexit of { } |
|
91 |
| Startquiet of { } |
|
92 |
| Stopquiet of { } |
|
93 |
| Pgmlsymbolson of { } |
|
94 |
| Pgmlsymbolsoff of { } |
|
22406
a591df440b5b
Add setproverflag, to replace other flag controls
aspinall
parents:
22161
diff
changeset
|
95 |
| Setproverflag of { flagname:string, value: bool } |
21637 | 96 |
(* improper proof commands: control proof state *) |
97 |
| Dostep of { text: string } |
|
98 |
| Undostep of { times: int } |
|
99 |
| Redostep of { } |
|
100 |
| Abortgoal of { } |
|
101 |
| Forget of { thyname: string option, name: string option, |
|
21867 | 102 |
objtype: PgipTypes.objtype option } |
21637 | 103 |
| Restoregoal of { thmname : string } |
104 |
(* context inspection commands *) |
|
21867 | 105 |
| Askids of { url: PgipTypes.pgipurl option, |
106 |
thyname: PgipTypes.objname option, |
|
107 |
objtype: PgipTypes.objtype option } |
|
22161 | 108 |
| Askrefs of { url: PgipTypes.pgipurl option, |
109 |
thyname: PgipTypes.objname option, |
|
110 |
objtype: PgipTypes.objtype option, |
|
111 |
name: PgipTypes.objname option } |
|
21867 | 112 |
| Showid of { thyname: PgipTypes.objname option, |
113 |
objtype: PgipTypes.objtype, |
|
114 |
name: PgipTypes.objname } |
|
21637 | 115 |
| Askguise of { } |
116 |
| Parsescript of { text: string, location: location, |
|
117 |
systemdata: string option } |
|
118 |
| Showproofstate of { } |
|
119 |
| Showctxt of { } |
|
120 |
| Searchtheorems of { arg: string } |
|
121 |
| Setlinewidth of { width: int } |
|
122 |
| Viewdoc of { arg: string } |
|
123 |
(* improper theory-level commands *) |
|
124 |
| Doitem of { text: string } |
|
125 |
| Undoitem of { } |
|
126 |
| Redoitem of { } |
|
127 |
| Aborttheory of { } |
|
128 |
| Retracttheory of { thyname: string } |
|
129 |
| Loadfile of { url: pgipurl } |
|
130 |
| Openfile of { url: pgipurl } |
|
131 |
| Closefile of { } |
|
132 |
| Abortfile of { } |
|
133 |
| Retractfile of { url: pgipurl } |
|
134 |
| Changecwd of { url: pgipurl } |
|
135 |
| Systemcmd of { arg: string } |
|
136 |
(* unofficial escape command for debugging *) |
|
137 |
| Quitpgip of { } |
|
138 |
||
139 |
(* Extracting content from input XML elements to make a PGIPinput *) |
|
140 |
local |
|
141 |
||
142 |
val thyname_attro = get_attr_opt "thyname" |
|
143 |
val thyname_attr = get_attr "thyname" |
|
144 |
val name_attr = get_attr "name" |
|
145 |
val name_attro = get_attr_opt "name" |
|
146 |
val thmname_attr = get_attr "thmname" |
|
22406
a591df440b5b
Add setproverflag, to replace other flag controls
aspinall
parents:
22161
diff
changeset
|
147 |
val flagname_attr = get_attr "flagname" |
a591df440b5b
Add setproverflag, to replace other flag controls
aspinall
parents:
22161
diff
changeset
|
148 |
val value_attr = get_attr "value" |
21637 | 149 |
|
21867 | 150 |
fun objtype_attro attrs = if has_attr "objtype" attrs then |
151 |
SOME (objtype_of_attrs attrs) |
|
152 |
else NONE |
|
153 |
||
154 |
fun pgipurl_attro attrs = if has_attr "url" attrs then |
|
155 |
SOME (pgipurl_of_attrs attrs) |
|
156 |
else NONE |
|
157 |
||
21637 | 158 |
val times_attr = read_pgipnat o (get_attr_dflt "times" "1") |
159 |
val prefcat_attr = get_attr_opt "prefcategory" |
|
160 |
||
21940 | 161 |
fun xmltext (XML.Text text :: ts) = text ^ xmltext ts |
21637 | 162 |
| xmltext [] = "" |
163 |
| xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)" |
|
164 |
||
165 |
exception Unknown |
|
166 |
exception NoAction |
|
167 |
in |
|
168 |
||
169 |
(* Return a valid PGIP input command. |
|
170 |
Raise PGIP exception for invalid data. |
|
171 |
Return NONE for unknown/unhandled commands. |
|
172 |
*) |
|
173 |
fun input (elem, attrs, data) = |
|
174 |
SOME |
|
175 |
(case elem of |
|
176 |
"askpgip" => Askpgip { } |
|
177 |
| "askpgml" => Askpgml { } |
|
178 |
| "askconfig" => Askconfig { } |
|
179 |
(* proverconfig *) |
|
180 |
| "askprefs" => Askprefs { } |
|
181 |
| "getpref" => Getpref { name = name_attr attrs, |
|
182 |
prefcategory = prefcat_attr attrs } |
|
183 |
| "setpref" => Setpref { name = name_attr attrs, |
|
184 |
prefcategory = prefcat_attr attrs, |
|
185 |
value = xmltext data } |
|
186 |
(* provercontrol *) |
|
187 |
| "proverinit" => Proverinit { } |
|
188 |
| "proverexit" => Proverexit { } |
|
189 |
| "startquiet" => Startquiet { } |
|
190 |
| "stopquiet" => Stopquiet { } |
|
191 |
| "pgmlsymbolson" => Pgmlsymbolson { } |
|
22083 | 192 |
| "pgmlsymbolsoff" => Pgmlsymbolsoff { } |
22406
a591df440b5b
Add setproverflag, to replace other flag controls
aspinall
parents:
22161
diff
changeset
|
193 |
| "setproverflag" => Setproverflag { flagname = flagname_attr attrs, |
a591df440b5b
Add setproverflag, to replace other flag controls
aspinall
parents:
22161
diff
changeset
|
194 |
value = read_pgipbool (value_attr attrs) } |
21637 | 195 |
(* improperproofcmd: improper commands not in script *) |
196 |
| "dostep" => Dostep { text = xmltext data } |
|
197 |
| "undostep" => Undostep { times = times_attr attrs } |
|
198 |
| "redostep" => Redostep { } |
|
199 |
| "abortgoal" => Abortgoal { } |
|
200 |
| "forget" => Forget { thyname = thyname_attro attrs, |
|
201 |
name = name_attro attrs, |
|
202 |
objtype = objtype_attro attrs } |
|
203 |
| "restoregoal" => Restoregoal { thmname = thmname_attr attrs} |
|
204 |
(* proofctxt: improper commands *) |
|
21867 | 205 |
| "askids" => Askids { url = pgipurl_attro attrs, |
206 |
thyname = thyname_attro attrs, |
|
21637 | 207 |
objtype = objtype_attro attrs } |
22161 | 208 |
| "askrefs" => Askrefs { url = pgipurl_attro attrs, |
209 |
thyname = thyname_attro attrs, |
|
210 |
objtype = objtype_attro attrs, |
|
211 |
name = name_attro attrs } |
|
21637 | 212 |
| "showid" => Showid { thyname = thyname_attro attrs, |
21867 | 213 |
objtype = objtype_of_attrs attrs, |
21637 | 214 |
name = name_attr attrs } |
215 |
| "askguise" => Askguise { } |
|
216 |
| "parsescript" => Parsescript { text = (xmltext data), |
|
217 |
systemdata = get_attr_opt "systemdata" attrs, |
|
218 |
location = location_of_attrs attrs } |
|
219 |
| "showproofstate" => Showproofstate { } |
|
220 |
| "showctxt" => Showctxt { } |
|
221 |
| "searchtheorems" => Searchtheorems { arg = xmltext data } |
|
222 |
| "setlinewidth" => Setlinewidth { width = read_pgipnat (xmltext data) } |
|
223 |
| "viewdoc" => Viewdoc { arg = xmltext data } |
|
224 |
(* improperfilecmd: theory-level commands not in script *) |
|
225 |
| "doitem" => Doitem { text = xmltext data } |
|
226 |
| "undoitem" => Undoitem { } |
|
227 |
| "redoitem" => Redoitem { } |
|
228 |
| "aborttheory" => Aborttheory { } |
|
229 |
| "retracttheory" => Retracttheory { thyname = thyname_attr attrs } |
|
230 |
| "loadfile" => Loadfile { url = pgipurl_of_attrs attrs } |
|
231 |
| "openfile" => Openfile { url = pgipurl_of_attrs attrs } |
|
232 |
| "closefile" => Closefile { } |
|
233 |
| "abortfile" => Abortfile { } |
|
234 |
| "retractfile" => Retractfile { url = pgipurl_of_attrs attrs } |
|
235 |
| "changecwd" => Changecwd { url = pgipurl_of_attrs attrs } |
|
236 |
| "systemcmd" => Systemcmd { arg = xmltext data } |
|
237 |
(* unofficial command for debugging *) |
|
238 |
| "quitpgip" => Quitpgip { } |
|
239 |
||
240 |
(* We allow sending proper document markup too; we map it back to dostep *) |
|
241 |
(* and strip out metainfo elements. Markup correctness isn't checked: this *) |
|
242 |
(* is a compatibility measure to make it easy for interfaces. *) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21649
diff
changeset
|
243 |
| x => if (x mem PgipMarkup.doc_markup_elements) then |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21649
diff
changeset
|
244 |
if (x mem PgipMarkup.doc_markup_elements_ignored) then |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21649
diff
changeset
|
245 |
raise NoAction |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21649
diff
changeset
|
246 |
else |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21649
diff
changeset
|
247 |
Dostep { text = xmltext data } (* could separate out Doitem too *) |
21637 | 248 |
else raise Unknown) |
249 |
handle Unknown => NONE | NoAction => NONE |
|
250 |
end |
|
251 |
||
252 |
end |