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