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