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