|
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 |