aspinall@21637
|
1 |
(* Title: Pure/ProofGeneral/proof_general_pgip.ML
|
aspinall@21637
|
2 |
ID: $Id$
|
aspinall@21637
|
3 |
Author: David Aspinall and Markus Wenzel
|
aspinall@21637
|
4 |
|
aspinall@21637
|
5 |
Isabelle configuration for Proof General using PGIP protocol.
|
wenzelm@21940
|
6 |
See http://proofgeneral.inf.ed.ac.uk/kit
|
aspinall@21637
|
7 |
*)
|
aspinall@21637
|
8 |
|
aspinall@21637
|
9 |
signature PROOF_GENERAL_PGIP =
|
aspinall@21637
|
10 |
sig
|
wenzelm@21940
|
11 |
val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *)
|
aspinall@21642
|
12 |
|
aspinall@21649
|
13 |
(* These two are just to support the semi-PGIP Emacs mode *)
|
wenzelm@21940
|
14 |
val init_pgip_channel: (string -> unit) -> unit
|
wenzelm@21940
|
15 |
val process_pgip: string -> unit
|
aspinall@22042
|
16 |
|
aspinall@23435
|
17 |
(* More message functions... *)
|
aspinall@23435
|
18 |
val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *)
|
wenzelm@22228
|
19 |
val log_msg : string -> unit (* for internal log messages *)
|
aspinall@23759
|
20 |
val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
|
aspinall@22159
|
21 |
|
aspinall@22163
|
22 |
val get_currently_open_file : unit -> Path.T option (* interface focus *)
|
aspinall@21637
|
23 |
end
|
aspinall@21637
|
24 |
|
aspinall@21637
|
25 |
structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
|
aspinall@21637
|
26 |
struct
|
aspinall@21637
|
27 |
|
aspinall@21637
|
28 |
open Pgip;
|
aspinall@21637
|
29 |
|
wenzelm@21949
|
30 |
|
wenzelm@23641
|
31 |
(** print mode **)
|
aspinall@21637
|
32 |
|
aspinall@22408
|
33 |
val proof_generalN = "ProofGeneral";
|
aspinall@22408
|
34 |
val pgmlsymbols_flag = ref true;
|
aspinall@21637
|
35 |
|
wenzelm@23641
|
36 |
|
wenzelm@23641
|
37 |
(* symbol output *)
|
wenzelm@23641
|
38 |
|
aspinall@21637
|
39 |
local
|
aspinall@21637
|
40 |
|
aspinall@21637
|
41 |
fun xsym_output "\\" = "\\\\"
|
aspinall@21637
|
42 |
| xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
|
aspinall@21637
|
43 |
|
aspinall@21637
|
44 |
fun pgml_sym s =
|
aspinall@21637
|
45 |
(case Symbol.decode s of
|
aspinall@21637
|
46 |
Symbol.Char s => XML.text s
|
aspinall@22408
|
47 |
| Symbol.Sym sn =>
|
aspinall@22408
|
48 |
let val ascii = implode (map xsym_output (Symbol.explode s))
|
aspinall@22408
|
49 |
in if !pgmlsymbols_flag then XML.element "sym" [("name", sn)] [XML.text ascii]
|
aspinall@22408
|
50 |
else ascii end
|
aspinall@22408
|
51 |
| Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text sn] (* FIXME: no such PGML *)
|
aspinall@22408
|
52 |
| Symbol.Raw raw => raw);
|
aspinall@21637
|
53 |
|
aspinall@21637
|
54 |
fun pgml_output str =
|
aspinall@21637
|
55 |
let val syms = Symbol.explode str
|
wenzelm@23621
|
56 |
in (implode (map pgml_sym syms), Symbol.length syms) end;
|
wenzelm@23621
|
57 |
|
aspinall@21637
|
58 |
in
|
aspinall@21637
|
59 |
|
aspinall@22408
|
60 |
fun setup_proofgeneral_output () =
|
wenzelm@23641
|
61 |
Output.add_mode proof_generalN pgml_output Symbol.encode_raw;
|
aspinall@21637
|
62 |
|
aspinall@21637
|
63 |
end;
|
aspinall@21637
|
64 |
|
aspinall@21637
|
65 |
|
aspinall@21637
|
66 |
(* token translations *)
|
aspinall@21637
|
67 |
|
aspinall@21637
|
68 |
local
|
aspinall@21637
|
69 |
|
aspinall@21637
|
70 |
val class_tag = "class"
|
aspinall@21637
|
71 |
val tfree_tag = "tfree"
|
aspinall@21637
|
72 |
val tvar_tag = "tvar"
|
aspinall@21637
|
73 |
val free_tag = "free"
|
aspinall@21637
|
74 |
val bound_tag = "bound"
|
aspinall@21637
|
75 |
val var_tag = "var"
|
aspinall@21637
|
76 |
val skolem_tag = "skolem"
|
aspinall@21637
|
77 |
|
aspinall@21637
|
78 |
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
|
aspinall@21637
|
79 |
|
wenzelm@21940
|
80 |
fun tagit kind x =
|
wenzelm@23621
|
81 |
(xml_atom kind x, Symbol.length (Symbol.explode x));
|
aspinall@21637
|
82 |
|
aspinall@21637
|
83 |
fun free_or_skolem x =
|
aspinall@21637
|
84 |
(case try Name.dest_skolem x of
|
aspinall@21637
|
85 |
NONE => tagit free_tag x
|
aspinall@21637
|
86 |
| SOME x' => tagit skolem_tag x');
|
aspinall@21637
|
87 |
|
aspinall@21637
|
88 |
fun var_or_skolem s =
|
wenzelm@24244
|
89 |
(case Lexicon.read_variable s of
|
aspinall@21637
|
90 |
SOME (x, i) =>
|
aspinall@21637
|
91 |
(case try Name.dest_skolem x of
|
aspinall@21637
|
92 |
NONE => tagit var_tag s
|
aspinall@21637
|
93 |
| SOME x' => tagit skolem_tag
|
wenzelm@22678
|
94 |
(setmp show_question_marks true Term.string_of_vname (x', i)))
|
aspinall@21637
|
95 |
| NONE => tagit var_tag s);
|
aspinall@21637
|
96 |
|
aspinall@21637
|
97 |
val proof_general_trans =
|
aspinall@21637
|
98 |
Syntax.tokentrans_mode proof_generalN
|
aspinall@21637
|
99 |
[("class", tagit class_tag),
|
aspinall@21637
|
100 |
("tfree", tagit tfree_tag),
|
aspinall@21637
|
101 |
("tvar", tagit tvar_tag),
|
aspinall@21637
|
102 |
("free", free_or_skolem),
|
aspinall@21637
|
103 |
("bound", tagit bound_tag),
|
aspinall@21637
|
104 |
("var", var_or_skolem)];
|
aspinall@21637
|
105 |
|
aspinall@21637
|
106 |
in
|
aspinall@21637
|
107 |
|
aspinall@21637
|
108 |
val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
|
aspinall@21637
|
109 |
|
aspinall@21637
|
110 |
end;
|
aspinall@21637
|
111 |
|
aspinall@21637
|
112 |
|
wenzelm@23641
|
113 |
(* assembling and issuing PGIP packets *)
|
aspinall@21637
|
114 |
|
aspinall@21637
|
115 |
val pgip_refid = ref NONE: string option ref;
|
aspinall@21637
|
116 |
val pgip_refseq = ref NONE: int option ref;
|
aspinall@21637
|
117 |
|
aspinall@21637
|
118 |
local
|
aspinall@21637
|
119 |
val pgip_class = "pg"
|
aspinall@21637
|
120 |
val pgip_tag = "Isabelle/Isar"
|
aspinall@21637
|
121 |
val pgip_id = ref ""
|
aspinall@21637
|
122 |
val pgip_seq = ref 0
|
aspinall@21637
|
123 |
fun pgip_serial () = inc pgip_seq
|
aspinall@21637
|
124 |
|
aspinall@21637
|
125 |
fun assemble_pgips pgips =
|
wenzelm@21940
|
126 |
Pgip { tag = SOME pgip_tag,
|
wenzelm@21940
|
127 |
class = pgip_class,
|
wenzelm@21940
|
128 |
seq = pgip_serial(),
|
wenzelm@21940
|
129 |
id = !pgip_id,
|
wenzelm@21940
|
130 |
destid = !pgip_refid,
|
wenzelm@21940
|
131 |
(* destid=refid since Isabelle only communicates back to sender *)
|
wenzelm@21940
|
132 |
refid = !pgip_refid,
|
wenzelm@21940
|
133 |
refseq = !pgip_refseq,
|
wenzelm@21940
|
134 |
content = pgips }
|
aspinall@21637
|
135 |
in
|
aspinall@21637
|
136 |
|
aspinall@21637
|
137 |
fun init_pgip_session_id () =
|
aspinall@21637
|
138 |
pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
|
aspinall@21637
|
139 |
getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
|
aspinall@21637
|
140 |
|
aspinall@21637
|
141 |
fun matching_pgip_id id = (id = !pgip_id)
|
aspinall@21637
|
142 |
|
wenzelm@22590
|
143 |
val output_xml_fn = ref Output.writeln_default
|
aspinall@21649
|
144 |
fun output_xml s = (!output_xml_fn) (XML.string_of_tree s); (* TODO: string buffer *)
|
aspinall@21637
|
145 |
|
wenzelm@23641
|
146 |
val output_pgips =
|
wenzelm@23641
|
147 |
XML.string_of_tree o PgipOutput.output o assemble_pgips o map PgipOutput.output;
|
wenzelm@23641
|
148 |
|
aspinall@23759
|
149 |
val output_pgmlterm =
|
aspinall@23759
|
150 |
XML.string_of_tree o Pgml.pgmlterm_to_xml;
|
aspinall@23759
|
151 |
|
aspinall@23759
|
152 |
val output_pgmltext =
|
aspinall@23759
|
153 |
XML.string_of_tree o Pgml.pgml_to_xml;
|
aspinall@23759
|
154 |
|
aspinall@23759
|
155 |
|
wenzelm@21940
|
156 |
fun issue_pgip_rawtext str =
|
wenzelm@23723
|
157 |
output_xml (PgipOutput.output (assemble_pgips [XML.Output str]))
|
aspinall@21637
|
158 |
|
aspinall@21637
|
159 |
fun issue_pgips pgipops =
|
aspinall@21637
|
160 |
output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
|
aspinall@21637
|
161 |
|
aspinall@21637
|
162 |
fun issue_pgip pgipop =
|
aspinall@21637
|
163 |
output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
|
aspinall@21637
|
164 |
|
aspinall@21637
|
165 |
end;
|
aspinall@21637
|
166 |
|
aspinall@21637
|
167 |
|
aspinall@23759
|
168 |
fun pgml area terms = Pgml.Pgml { version=NONE,systemid=NONE,
|
wenzelm@23801
|
169 |
area=SOME area, content=terms }
|
wenzelm@23641
|
170 |
|
aspinall@21637
|
171 |
(** messages and notification **)
|
aspinall@21637
|
172 |
|
aspinall@21637
|
173 |
local
|
aspinall@21637
|
174 |
val delay_msgs = ref false (*true: accumulate messages*)
|
aspinall@21637
|
175 |
val delayed_msgs = ref []
|
aspinall@21637
|
176 |
|
aspinall@21637
|
177 |
fun queue_or_issue pgip =
|
wenzelm@21940
|
178 |
if ! delay_msgs then
|
wenzelm@21940
|
179 |
delayed_msgs := pgip :: ! delayed_msgs
|
wenzelm@21940
|
180 |
else issue_pgip pgip
|
aspinall@23759
|
181 |
|
aspinall@23759
|
182 |
fun wrap_pgml area s =
|
wenzelm@23801
|
183 |
if String.isPrefix "<pgml" s then
|
wenzelm@23801
|
184 |
XML.Output s (* already pgml outermost *)
|
wenzelm@23801
|
185 |
else
|
wenzelm@23801
|
186 |
Pgml.pgml_to_xml (pgml area [Pgml.Raw (XML.Output s)]) (* mixed *)
|
aspinall@23759
|
187 |
|
aspinall@21637
|
188 |
in
|
aspinall@23759
|
189 |
fun normalmsg area s =
|
wenzelm@21940
|
190 |
let
|
aspinall@23759
|
191 |
val content = wrap_pgml area s
|
aspinall@23759
|
192 |
val pgip = Normalresponse { content=[content] }
|
wenzelm@21940
|
193 |
in
|
wenzelm@21940
|
194 |
queue_or_issue pgip
|
wenzelm@21940
|
195 |
end
|
aspinall@21637
|
196 |
|
aspinall@23759
|
197 |
fun errormsg area fatality s =
|
wenzelm@21940
|
198 |
let
|
aspinall@23759
|
199 |
val content = wrap_pgml area s
|
aspinall@23759
|
200 |
val pgip = Errorresponse { fatality=fatality,
|
aspinall@23759
|
201 |
location=NONE,
|
aspinall@23759
|
202 |
content=[content] }
|
wenzelm@21940
|
203 |
in
|
wenzelm@21940
|
204 |
queue_or_issue pgip
|
wenzelm@21940
|
205 |
end
|
aspinall@21637
|
206 |
|
aspinall@22159
|
207 |
(* Error responses with useful locations *)
|
aspinall@23759
|
208 |
fun error_with_pos area fatality pos s =
|
aspinall@22159
|
209 |
let
|
aspinall@23759
|
210 |
val content = wrap_pgml area s
|
aspinall@23759
|
211 |
val pgip = Errorresponse { fatality=fatality,
|
aspinall@23759
|
212 |
location=SOME (PgipIsabelle.location_of_position pos),
|
aspinall@23759
|
213 |
content=[content] }
|
aspinall@22159
|
214 |
in
|
aspinall@22159
|
215 |
queue_or_issue pgip
|
aspinall@22159
|
216 |
end
|
aspinall@22159
|
217 |
|
aspinall@21637
|
218 |
fun start_delay_msgs () = (set delay_msgs; delayed_msgs := [])
|
aspinall@21637
|
219 |
fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs)
|
aspinall@21637
|
220 |
end;
|
aspinall@21637
|
221 |
|
aspinall@21637
|
222 |
(* NB: all of the standard error/message functions now expect already-escaped text.
|
aspinall@21637
|
223 |
FIXME: this may cause us problems now we're generating trees; on the other
|
wenzelm@21940
|
224 |
hand the output functions were tuned some time ago, so it ought to be
|
aspinall@23759
|
225 |
enough to use XML.Output always above. *)
|
aspinall@22042
|
226 |
(* NB 2: all of standard functions print strings terminated with new lines, but we don't
|
wenzelm@22228
|
227 |
add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
|
aspinall@22042
|
228 |
can't be written without newlines. *)
|
aspinall@21637
|
229 |
|
aspinall@21637
|
230 |
fun setup_messages () =
|
aspinall@23759
|
231 |
(Output.writeln_fn := (fn s => normalmsg Message s);
|
aspinall@23840
|
232 |
Output.priority_fn := (fn s => normalmsg Status s);
|
aspinall@23840
|
233 |
Output.tracing_fn := (fn s => normalmsg Tracing s);
|
aspinall@23759
|
234 |
Output.warning_fn := (fn s => errormsg Message Warning s);
|
aspinall@23759
|
235 |
Output.error_fn := (fn s => errormsg Message Fatal s);
|
aspinall@23759
|
236 |
Output.debug_fn := (fn s => errormsg Message Debug s));
|
aspinall@22042
|
237 |
|
aspinall@23759
|
238 |
fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
|
aspinall@23759
|
239 |
fun nonfatal_error s = errormsg Message Nonfatal s;
|
aspinall@23759
|
240 |
fun log_msg s = errormsg Message Log s;
|
aspinall@21983
|
241 |
|
aspinall@21637
|
242 |
|
aspinall@21637
|
243 |
(* immediate messages *)
|
aspinall@21637
|
244 |
|
aspinall@23759
|
245 |
fun tell_clear_goals () =
|
aspinall@23759
|
246 |
issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
|
aspinall@23759
|
247 |
fun tell_clear_response () =
|
aspinall@23759
|
248 |
issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
|
aspinall@22042
|
249 |
|
wenzelm@22228
|
250 |
fun tell_file_loaded completed path =
|
aspinall@22042
|
251 |
issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
|
wenzelm@22228
|
252 |
completed=completed})
|
wenzelm@22228
|
253 |
fun tell_file_outdated completed path =
|
aspinall@22042
|
254 |
issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
|
wenzelm@22228
|
255 |
completed=completed})
|
wenzelm@22228
|
256 |
fun tell_file_retracted completed path =
|
aspinall@22042
|
257 |
issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
|
wenzelm@22228
|
258 |
completed=completed})
|
aspinall@21637
|
259 |
|
aspinall@21637
|
260 |
|
wenzelm@23641
|
261 |
(* common markup *)
|
aspinall@21637
|
262 |
|
aspinall@21637
|
263 |
local
|
aspinall@21637
|
264 |
|
wenzelm@23641
|
265 |
val no_text = chr 0;
|
wenzelm@23641
|
266 |
|
aspinall@23759
|
267 |
val pgmlterms_no_text= [Pgml.Raw (XML.Output no_text)]
|
aspinall@23759
|
268 |
|
wenzelm@23641
|
269 |
fun split_markup text =
|
wenzelm@23641
|
270 |
(case space_explode no_text text of
|
wenzelm@23641
|
271 |
[bg, en] => (bg, en)
|
aspinall@23759
|
272 |
| _ => (error ("Internal error: failed to split XML markup:\n" ^ text); ("", "")));
|
wenzelm@23641
|
273 |
|
aspinall@23759
|
274 |
|
wenzelm@23801
|
275 |
fun block_markup markup =
|
aspinall@23759
|
276 |
let
|
wenzelm@23801
|
277 |
val pgml = Pgml.Box { orient = NONE,
|
wenzelm@23801
|
278 |
indent = Markup.get_int markup Markup.indentN,
|
wenzelm@23801
|
279 |
content = pgmlterms_no_text }
|
aspinall@23759
|
280 |
in split_markup (output_pgmlterm pgml) end;
|
aspinall@23759
|
281 |
|
wenzelm@23801
|
282 |
fun break_markup markup =
|
aspinall@23759
|
283 |
let
|
wenzelm@23801
|
284 |
val pgml = Pgml.Break { mandatory = NONE,
|
wenzelm@23801
|
285 |
indent = Markup.get_int markup Markup.widthN }
|
aspinall@23759
|
286 |
in (output_pgmlterm pgml, "") end;
|
aspinall@23759
|
287 |
|
wenzelm@23801
|
288 |
fun fbreak_markup markup =
|
aspinall@23759
|
289 |
let
|
wenzelm@23801
|
290 |
val pgml = Pgml.Break { mandatory = SOME true, indent = NONE }
|
aspinall@23759
|
291 |
in (output_pgmlterm pgml, "") end;
|
aspinall@23759
|
292 |
|
aspinall@23759
|
293 |
val state_markup =
|
aspinall@23759
|
294 |
split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
|
aspinall@21637
|
295 |
|
wenzelm@23801
|
296 |
fun proof_general_markup (markup as (name, _)) =
|
wenzelm@23801
|
297 |
if name = Markup.blockN then block_markup markup
|
wenzelm@23801
|
298 |
else if name = Markup.breakN then break_markup markup
|
wenzelm@23801
|
299 |
else if name = Markup.fbreakN then fbreak_markup markup
|
wenzelm@23801
|
300 |
(* else if name = Markup.classN then class_markup markup
|
wenzelm@23801
|
301 |
else if name = Markup.tyconN then tycon_markup markup
|
wenzelm@23801
|
302 |
else if name = Markup.constN then const_markup markup
|
wenzelm@23801
|
303 |
else if name = Markup.axiomN then axiom_markup markup
|
wenzelm@23801
|
304 |
else if name = Markup.sortN then sort_markup markup
|
wenzelm@23801
|
305 |
else if name = Markup.typN then typ_markup markup
|
wenzelm@23801
|
306 |
else if name = Markup.termN then term_markup markup
|
wenzelm@23801
|
307 |
else if name = Markup.keywordN then keyword_markup markup
|
wenzelm@23801
|
308 |
else if name = Markup.commandN then command_markup markup
|
wenzelm@23801
|
309 |
else if name = Markup.promptN then prompt_markup markup *)
|
aspinall@23759
|
310 |
else if name = Markup.stateN then state_markup
|
aspinall@23759
|
311 |
(* else if name = Markup.subgoalN then subgoal_markup () *)
|
wenzelm@23801
|
312 |
else ("", "");
|
aspinall@21637
|
313 |
|
aspinall@21637
|
314 |
in
|
aspinall@21637
|
315 |
|
wenzelm@23702
|
316 |
val _ = Markup.add_mode proof_generalN proof_general_markup;
|
aspinall@21637
|
317 |
|
aspinall@21637
|
318 |
end;
|
aspinall@21637
|
319 |
|
aspinall@21637
|
320 |
|
aspinall@21637
|
321 |
(* theory loader actions *)
|
aspinall@21637
|
322 |
|
aspinall@21637
|
323 |
local
|
wenzelm@22228
|
324 |
(* da: TODO: PGIP has a completed flag so the prover can indicate to the
|
wenzelm@22228
|
325 |
interface which files are busy performing a particular action.
|
aspinall@22042
|
326 |
To make use of this we need to adjust the hook in thy_info.ML
|
wenzelm@22228
|
327 |
(may actually be difficult to tell the interface *which* action is in
|
aspinall@22042
|
328 |
progress, but we could add a generic "Lock" action which uses
|
aspinall@22042
|
329 |
informfileloaded: the broker/UI should not infer too much from incomplete
|
aspinall@22042
|
330 |
operations).
|
wenzelm@22228
|
331 |
*)
|
aspinall@21637
|
332 |
fun trace_action action name =
|
aspinall@21637
|
333 |
if action = ThyInfo.Update then
|
wenzelm@22228
|
334 |
List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
|
aspinall@22042
|
335 |
else if action = ThyInfo.Outdate then
|
aspinall@22042
|
336 |
List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
|
aspinall@22042
|
337 |
else if action = ThyInfo.Remove then
|
wenzelm@22228
|
338 |
List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
|
aspinall@22042
|
339 |
else ()
|
aspinall@22042
|
340 |
|
aspinall@21637
|
341 |
|
aspinall@21637
|
342 |
in
|
aspinall@21637
|
343 |
fun setup_thy_loader () = ThyInfo.add_hook trace_action;
|
aspinall@21637
|
344 |
fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
|
aspinall@21637
|
345 |
end;
|
aspinall@21637
|
346 |
|
aspinall@21637
|
347 |
|
wenzelm@21949
|
348 |
(* get informed about files *)
|
aspinall@21637
|
349 |
|
aspinall@22042
|
350 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
|
aspinall@21637
|
351 |
|
aspinall@21637
|
352 |
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
|
aspinall@21637
|
353 |
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
|
aspinall@21637
|
354 |
|
aspinall@22042
|
355 |
fun proper_inform_file_processed path state =
|
aspinall@22042
|
356 |
let val name = thy_name path in
|
aspinall@21637
|
357 |
if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
|
aspinall@21637
|
358 |
(ThyInfo.touch_child_thys name;
|
wenzelm@24079
|
359 |
ThyInfo.register_thy name handle ERROR msg =>
|
wenzelm@23913
|
360 |
(warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
|
aspinall@22042
|
361 |
tell_file_retracted true (Path.base path)))
|
aspinall@21637
|
362 |
else raise Toplevel.UNDEF
|
aspinall@21637
|
363 |
end;
|
aspinall@21637
|
364 |
|
aspinall@21637
|
365 |
|
aspinall@21637
|
366 |
(* restart top-level loop (keeps most state information) *)
|
aspinall@21637
|
367 |
|
aspinall@21637
|
368 |
val welcome = priority o Session.welcome;
|
aspinall@21637
|
369 |
|
aspinall@21637
|
370 |
fun restart () =
|
aspinall@21637
|
371 |
(sync_thy_loader ();
|
aspinall@21637
|
372 |
tell_clear_goals ();
|
aspinall@21637
|
373 |
tell_clear_response ();
|
aspinall@21637
|
374 |
welcome ();
|
aspinall@21637
|
375 |
raise Toplevel.RESTART)
|
aspinall@21637
|
376 |
|
aspinall@21637
|
377 |
|
aspinall@21637
|
378 |
(* theorem dependency output *)
|
aspinall@22408
|
379 |
|
aspinall@22408
|
380 |
val show_theorem_dependencies = ref false;
|
aspinall@22408
|
381 |
|
aspinall@21637
|
382 |
local
|
aspinall@21637
|
383 |
|
aspinall@21637
|
384 |
val spaces_quote = space_implode " " o map quote;
|
aspinall@21637
|
385 |
|
aspinall@21637
|
386 |
fun thm_deps_message (thms, deps) =
|
wenzelm@21940
|
387 |
let
|
wenzelm@21940
|
388 |
val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
|
wenzelm@21940
|
389 |
val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
|
aspinall@21637
|
390 |
in
|
wenzelm@21940
|
391 |
issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
|
wenzelm@21940
|
392 |
content=[valuethms,valuedeps]})
|
aspinall@21637
|
393 |
end
|
aspinall@21637
|
394 |
|
wenzelm@21969
|
395 |
fun tell_thm_deps ths =
|
aspinall@22408
|
396 |
if !show_theorem_dependencies then
|
wenzelm@22228
|
397 |
let
|
wenzelm@22228
|
398 |
val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
|
wenzelm@22228
|
399 |
val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
|
wenzelm@22228
|
400 |
(map Thm.proof_of ths) Symtab.empty))
|
wenzelm@22228
|
401 |
in
|
wenzelm@22228
|
402 |
if null names orelse null deps then ()
|
wenzelm@22228
|
403 |
else thm_deps_message (spaces_quote names, spaces_quote deps)
|
aspinall@22225
|
404 |
end
|
aspinall@22225
|
405 |
else ()
|
aspinall@21637
|
406 |
|
aspinall@21637
|
407 |
in
|
aspinall@21637
|
408 |
|
aspinall@21637
|
409 |
fun setup_present_hook () =
|
aspinall@21637
|
410 |
Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
|
aspinall@21637
|
411 |
|
aspinall@21637
|
412 |
end;
|
aspinall@21637
|
413 |
|
aspinall@21637
|
414 |
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
|
aspinall@21637
|
415 |
|
wenzelm@21940
|
416 |
fun lexicalstructure_keywords () =
|
aspinall@21637
|
417 |
let val commands = OuterSyntax.dest_keywords ()
|
wenzelm@21940
|
418 |
fun category_of k = if k mem commands then "major" else "minor"
|
aspinall@21637
|
419 |
(* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
|
wenzelm@21940
|
420 |
fun keyword_elt (keyword,help,kind,_) =
|
wenzelm@21940
|
421 |
XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
|
wenzelm@21940
|
422 |
[XML.Elem("shorthelp", [], [XML.Text help])])
|
wenzelm@21940
|
423 |
in
|
aspinall@21637
|
424 |
(* Also, note we don't call init_outer_syntax here to add interface commands,
|
aspinall@21637
|
425 |
but they should never appear in scripts anyway so it shouldn't matter *)
|
aspinall@21637
|
426 |
Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
|
aspinall@21637
|
427 |
end
|
aspinall@21637
|
428 |
|
aspinall@21637
|
429 |
(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
|
aspinall@21637
|
430 |
hooks needed in outer_syntax.ML to do that. *)
|
aspinall@21637
|
431 |
|
aspinall@21637
|
432 |
|
aspinall@21637
|
433 |
(* Configuration: GUI config, proverinfo messages *)
|
aspinall@21637
|
434 |
|
aspinall@21637
|
435 |
local
|
aspinall@21637
|
436 |
val isabellewww = "http://isabelle.in.tum.de/"
|
aspinall@21637
|
437 |
val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
|
wenzelm@21940
|
438 |
fun orenv v d = case getenv v of "" => d | s => s
|
aspinall@21637
|
439 |
fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
|
aspinall@21637
|
440 |
fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
|
aspinall@21637
|
441 |
in
|
aspinall@21637
|
442 |
fun send_pgip_config () =
|
aspinall@21637
|
443 |
let
|
wenzelm@21858
|
444 |
val path = Path.explode (config_file())
|
wenzelm@21940
|
445 |
val ex = File.exists path
|
aspinall@21637
|
446 |
|
wenzelm@21940
|
447 |
val wwwpage =
|
wenzelm@21940
|
448 |
(Url.explode (isabelle_www()))
|
wenzelm@21969
|
449 |
handle ERROR _ =>
|
wenzelm@22699
|
450 |
(panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
|
wenzelm@21940
|
451 |
Url.explode isabellewww)
|
wenzelm@21940
|
452 |
|
wenzelm@21940
|
453 |
val proverinfo =
|
aspinall@21637
|
454 |
Proverinfo { name = "Isabelle",
|
wenzelm@21940
|
455 |
version = version,
|
wenzelm@21940
|
456 |
instance = Session.name(),
|
wenzelm@21940
|
457 |
descr = "The Isabelle/Isar theorem prover",
|
wenzelm@21940
|
458 |
url = wwwpage,
|
wenzelm@21940
|
459 |
filenameextns = ".thy;" }
|
aspinall@21637
|
460 |
in
|
wenzelm@21940
|
461 |
if ex then
|
wenzelm@21940
|
462 |
(issue_pgip proverinfo;
|
wenzelm@21940
|
463 |
issue_pgip_rawtext (File.read path);
|
wenzelm@21940
|
464 |
issue_pgip (lexicalstructure_keywords()))
|
wenzelm@22699
|
465 |
else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
|
aspinall@21637
|
466 |
end;
|
aspinall@21637
|
467 |
end
|
aspinall@21637
|
468 |
|
aspinall@21637
|
469 |
|
aspinall@22216
|
470 |
(* Preferences: tweak for PGIP interfaces *)
|
aspinall@22216
|
471 |
|
aspinall@22216
|
472 |
val preferences = ref Preferences.preferences;
|
aspinall@22216
|
473 |
|
aspinall@22216
|
474 |
fun setup_preferences_tweak() =
|
aspinall@22216
|
475 |
preferences :=
|
aspinall@22216
|
476 |
(!preferences |> Preferences.set_default ("show-question-marks","false")
|
aspinall@22408
|
477 |
|> Preferences.remove "show-question-marks" (* we use markup, not ?s *)
|
wenzelm@22590
|
478 |
|> Preferences.remove "theorem-dependencies" (* set internally *)
|
wenzelm@22590
|
479 |
|> Preferences.remove "full-proofs") (* set internally *)
|
wenzelm@22228
|
480 |
|
aspinall@21637
|
481 |
|
aspinall@21637
|
482 |
|
aspinall@21637
|
483 |
(* Sending commands to Isar *)
|
aspinall@21637
|
484 |
|
aspinall@21637
|
485 |
fun isarcmd s =
|
aspinall@21637
|
486 |
s |> OuterSyntax.scan |> OuterSyntax.read
|
wenzelm@23681
|
487 |
(*|> map (Toplevel.position Position.none o #3)*)
|
aspinall@21885
|
488 |
|> map #3
|
aspinall@21885
|
489 |
|> Toplevel.>>>;
|
aspinall@21637
|
490 |
|
wenzelm@21940
|
491 |
(* TODO:
|
aspinall@21885
|
492 |
- apply a command given a transition function, e.g. IsarCmd.undo.
|
aspinall@21885
|
493 |
- fix position from path of currently open file [line numbers risk garbling though].
|
aspinall@21885
|
494 |
*)
|
aspinall@21637
|
495 |
|
aspinall@21637
|
496 |
(* load an arbitrary file (must be .thy or .ML) *)
|
aspinall@21637
|
497 |
|
aspinall@21637
|
498 |
fun use_thy_or_ml_file file =
|
aspinall@21637
|
499 |
let
|
wenzelm@21858
|
500 |
val (path,extn) = Path.split_ext (Path.explode file)
|
aspinall@21637
|
501 |
in
|
aspinall@21637
|
502 |
case extn of
|
wenzelm@21940
|
503 |
"" => isarcmd ("use_thy " ^ quote (Path.implode path))
|
wenzelm@21940
|
504 |
| "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
|
aspinall@21637
|
505 |
| "ML" => isarcmd ("use " ^ quote file)
|
aspinall@22028
|
506 |
| other => error ("Don't know how to read a file with extension " ^ quote other)
|
aspinall@21637
|
507 |
end
|
aspinall@21637
|
508 |
|
aspinall@21637
|
509 |
|
aspinall@21867
|
510 |
(******* PGIP actions *******)
|
aspinall@21637
|
511 |
|
aspinall@21637
|
512 |
|
wenzelm@21940
|
513 |
(* Responses to each of the PGIP input commands.
|
aspinall@21637
|
514 |
These are programmed uniformly for extensibility. *)
|
aspinall@21637
|
515 |
|
wenzelm@23834
|
516 |
fun askpgip (Askpgip _) =
|
aspinall@23435
|
517 |
(issue_pgip
|
aspinall@23435
|
518 |
(Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
|
aspinall@23435
|
519 |
pgipelems = PgipIsabelle.accepted_inputs });
|
aspinall@23435
|
520 |
send_pgip_config())
|
aspinall@21637
|
521 |
|
wenzelm@23834
|
522 |
fun askpgml (Askpgml _) =
|
aspinall@21637
|
523 |
issue_pgip
|
wenzelm@21940
|
524 |
(Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
|
aspinall@21637
|
525 |
|
wenzelm@23834
|
526 |
fun askprefs (Askprefs _) =
|
wenzelm@21940
|
527 |
let
|
wenzelm@21940
|
528 |
fun preference_of {name, descr, default, pgiptype, get, set } =
|
wenzelm@21940
|
529 |
{ name = name, descr = SOME descr, default = SOME default,
|
wenzelm@21940
|
530 |
pgiptype = pgiptype }
|
aspinall@21637
|
531 |
in
|
wenzelm@21940
|
532 |
List.app (fn (prefcat, prefs) =>
|
wenzelm@21940
|
533 |
issue_pgip (Hasprefs {prefcategory=SOME prefcat,
|
wenzelm@21940
|
534 |
prefs=map preference_of prefs}))
|
aspinall@22216
|
535 |
(!preferences)
|
wenzelm@21940
|
536 |
end
|
aspinall@21637
|
537 |
|
wenzelm@23834
|
538 |
fun askconfig (Askconfig _) = () (* TODO: add config response *)
|
aspinall@21637
|
539 |
|
aspinall@21637
|
540 |
local
|
wenzelm@21940
|
541 |
fun lookuppref pref =
|
wenzelm@21940
|
542 |
case AList.lookup (op =)
|
wenzelm@21940
|
543 |
(map (fn p => (#name p,p))
|
aspinall@22216
|
544 |
(maps snd (!preferences))) pref of
|
wenzelm@21940
|
545 |
NONE => error ("Unknown prover preference: " ^ quote pref)
|
wenzelm@21940
|
546 |
| SOME p => p
|
aspinall@21637
|
547 |
in
|
wenzelm@21940
|
548 |
fun setpref (Setpref vs) =
|
wenzelm@21940
|
549 |
let
|
wenzelm@21940
|
550 |
val name = #name vs
|
wenzelm@21940
|
551 |
val value = #value vs
|
wenzelm@21940
|
552 |
val set = #set (lookuppref name)
|
aspinall@21637
|
553 |
in
|
wenzelm@21940
|
554 |
set value
|
aspinall@21637
|
555 |
end
|
aspinall@21637
|
556 |
|
haftmann@21902
|
557 |
fun getpref (Getpref vs) =
|
wenzelm@21940
|
558 |
let
|
wenzelm@21940
|
559 |
val name = #name vs
|
wenzelm@21940
|
560 |
val get = #get (lookuppref name)
|
wenzelm@21940
|
561 |
in
|
aspinall@21637
|
562 |
issue_pgip (Prefval {name=name, value=get ()})
|
aspinall@21637
|
563 |
end
|
aspinall@21637
|
564 |
end
|
aspinall@21637
|
565 |
|
wenzelm@23834
|
566 |
fun proverinit _ = restart ()
|
aspinall@21637
|
567 |
|
wenzelm@23834
|
568 |
fun proverexit _ = isarcmd "quit"
|
aspinall@21637
|
569 |
|
aspinall@22408
|
570 |
fun set_proverflag_quiet b =
|
aspinall@22408
|
571 |
isarcmd (if b then "disable_pr" else "enable_pr")
|
aspinall@21637
|
572 |
|
aspinall@22408
|
573 |
fun set_proverflag_pgmlsymbols b =
|
aspinall@22408
|
574 |
(pgmlsymbols_flag := b;
|
wenzelm@24614
|
575 |
NAMED_CRITICAL "print_mode" (fn () =>
|
wenzelm@24614
|
576 |
change print_mode
|
wenzelm@22590
|
577 |
(fn mode =>
|
wenzelm@24614
|
578 |
remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
|
aspinall@21637
|
579 |
|
aspinall@22408
|
580 |
fun set_proverflag_thmdeps b =
|
aspinall@22408
|
581 |
(show_theorem_dependencies := b;
|
aspinall@22408
|
582 |
proofs := (if b then 1 else 2))
|
aspinall@21637
|
583 |
|
aspinall@22408
|
584 |
fun setproverflag (Setproverflag vs) =
|
aspinall@22408
|
585 |
let
|
wenzelm@22590
|
586 |
val flagname = #flagname vs
|
wenzelm@22590
|
587 |
val value = #value vs
|
aspinall@22408
|
588 |
in
|
wenzelm@22590
|
589 |
(case flagname of
|
wenzelm@22590
|
590 |
"quiet" => set_proverflag_quiet value
|
wenzelm@22590
|
591 |
| "pgmlsymbols" => set_proverflag_pgmlsymbols value
|
wenzelm@22590
|
592 |
| "metainfo:thmdeps" => set_proverflag_thmdeps value
|
aspinall@23435
|
593 |
| _ => log_msg ("Unrecognised prover control flag: " ^
|
wenzelm@23801
|
594 |
(quote flagname) ^ " ignored."))
|
aspinall@22408
|
595 |
end
|
aspinall@22408
|
596 |
|
aspinall@21637
|
597 |
|
wenzelm@21940
|
598 |
fun dostep (Dostep vs) =
|
wenzelm@21940
|
599 |
let
|
wenzelm@21940
|
600 |
val text = #text vs
|
wenzelm@21940
|
601 |
in
|
wenzelm@21940
|
602 |
isarcmd text
|
aspinall@21637
|
603 |
end
|
aspinall@21637
|
604 |
|
haftmann@21902
|
605 |
fun undostep (Undostep vs) =
|
wenzelm@21940
|
606 |
let
|
wenzelm@21940
|
607 |
val times = #times vs
|
wenzelm@21940
|
608 |
in
|
wenzelm@21940
|
609 |
isarcmd ("undos_proof " ^ Int.toString times)
|
aspinall@21637
|
610 |
end
|
aspinall@21637
|
611 |
|
wenzelm@23834
|
612 |
fun redostep _ = isarcmd "redo"
|
wenzelm@21940
|
613 |
|
wenzelm@23834
|
614 |
fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
|
aspinall@21637
|
615 |
|
aspinall@21637
|
616 |
|
aspinall@21867
|
617 |
(*** PGIP identifier tables ***)
|
aspinall@21867
|
618 |
|
wenzelm@22228
|
619 |
(* TODO: these ones should be triggered by hooks after a
|
aspinall@22159
|
620 |
declaration addition/removal, to be sent automatically. *)
|
aspinall@21867
|
621 |
|
aspinall@22159
|
622 |
fun addids t = issue_pgip (Addids {idtables = [t]})
|
aspinall@22159
|
623 |
fun delids t = issue_pgip (Delids {idtables = [t]})
|
aspinall@21867
|
624 |
|
wenzelm@21940
|
625 |
fun askids (Askids vs) =
|
aspinall@21637
|
626 |
let
|
wenzelm@21940
|
627 |
val url = #url vs (* ask for identifiers within a file *)
|
wenzelm@21940
|
628 |
val thyname = #thyname vs (* ask for identifiers within a theory *)
|
wenzelm@21940
|
629 |
val objtype = #objtype vs (* ask for identifiers of a particular type *)
|
aspinall@21867
|
630 |
|
wenzelm@21940
|
631 |
fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
|
aspinall@21867
|
632 |
|
wenzelm@22228
|
633 |
fun setids t = issue_pgip (Setids {idtables = [t]})
|
aspinall@22159
|
634 |
|
aspinall@22225
|
635 |
(* fake one-level nested "subtheories" by picking apart names. *)
|
wenzelm@22228
|
636 |
val thms_of_thy =
|
wenzelm@22243
|
637 |
map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory
|
wenzelm@22243
|
638 |
val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
|
aspinall@22225
|
639 |
fun thy_prefix s = case space_explode NameSpace.separator s of
|
wenzelm@22228
|
640 |
x::_::_ => SOME x (* String.find? *)
|
wenzelm@22228
|
641 |
| _ => NONE
|
wenzelm@22228
|
642 |
fun subthys_of_thy s =
|
wenzelm@23178
|
643 |
List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
|
wenzelm@22228
|
644 |
(map thy_prefix (thms_of_thy s))
|
wenzelm@22228
|
645 |
fun subthms_of_thy thy =
|
wenzelm@22228
|
646 |
(case thy_prefix thy of
|
wenzelm@22228
|
647 |
NONE => immed_thms_of_thy thy
|
wenzelm@22228
|
648 |
| SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
|
wenzelm@22228
|
649 |
(thms_of_thy prf))
|
aspinall@22225
|
650 |
val qualified_thms_of_thy = (* for global query with single response *)
|
wenzelm@22590
|
651 |
(map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
|
aspinall@22249
|
652 |
(* da: this version is equivalent to my previous, but splits up theorem sets with names
|
aspinall@22249
|
653 |
that I can't get to access later with get_thm. Anyway, would rather use sets.
|
aspinall@22249
|
654 |
Is above right way to get qualified names in that case? Filtering required again?
|
wenzelm@22228
|
655 |
map PureThy.get_name_hint o filter PureThy.has_name_hint o
|
aspinall@22249
|
656 |
map snd o PureThy.thms_of o ThyInfo.get_theory; *)
|
aspinall@22249
|
657 |
in
|
wenzelm@21940
|
658 |
case (thyname,objtype) of
|
wenzelm@22228
|
659 |
(NONE, NONE) =>
|
wenzelm@22228
|
660 |
setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
|
wenzelm@22228
|
661 |
| (NONE, SOME ObjFile) =>
|
wenzelm@22228
|
662 |
setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
|
wenzelm@22228
|
663 |
| (SOME fi, SOME ObjFile) =>
|
wenzelm@22228
|
664 |
setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
|
aspinall@22225
|
665 |
| (NONE, SOME ObjTheory) =>
|
wenzelm@22228
|
666 |
setids (idtable ObjTheory NONE (ThyInfo.names()))
|
aspinall@22225
|
667 |
| (SOME thy, SOME ObjTheory) =>
|
wenzelm@22228
|
668 |
setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
|
wenzelm@22228
|
669 |
| (SOME thy, SOME ObjTheorem) =>
|
wenzelm@22228
|
670 |
setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
|
wenzelm@22228
|
671 |
| (NONE, SOME ObjTheorem) =>
|
wenzelm@22228
|
672 |
(* A large query, but not unreasonable. ~5000 results for HOL.*)
|
wenzelm@22228
|
673 |
(* Several setids should be allowed, but Eclipse code is currently broken:
|
wenzelm@23226
|
674 |
List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
|
wenzelm@22228
|
675 |
(ThyInfo.names()) *)
|
aspinall@22225
|
676 |
setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
|
wenzelm@22228
|
677 |
(maps qualified_thms_of_thy (ThyInfo.names())))
|
aspinall@22225
|
678 |
| _ => warning ("askids: ignored argument combination")
|
aspinall@21637
|
679 |
end
|
aspinall@21637
|
680 |
|
aspinall@22159
|
681 |
fun askrefs (Askrefs vs) =
|
aspinall@22159
|
682 |
let
|
aspinall@22159
|
683 |
val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *)
|
aspinall@22159
|
684 |
val thyname = #thyname vs (* ask for references of a theory (other theories) *)
|
aspinall@22159
|
685 |
val objtype = #objtype vs (* ask for references of a particular type... *)
|
aspinall@22159
|
686 |
val name = #name vs (* ... with this name *)
|
aspinall@22159
|
687 |
|
aspinall@22159
|
688 |
fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
|
aspinall@22159
|
689 |
|
aspinall@22159
|
690 |
val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory
|
aspinall@22159
|
691 |
|
wenzelm@22228
|
692 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base
|
aspinall@22159
|
693 |
|
wenzelm@22228
|
694 |
fun filerefs f =
|
wenzelm@22228
|
695 |
let val thy = thy_name f
|
wenzelm@24189
|
696 |
val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
|
wenzelm@22228
|
697 |
in
|
wenzelm@22228
|
698 |
issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
|
wenzelm@22228
|
699 |
name=NONE, idtables=[], fileurls=filerefs})
|
wenzelm@22228
|
700 |
end
|
aspinall@22159
|
701 |
|
wenzelm@22228
|
702 |
fun thyrefs thy =
|
wenzelm@24189
|
703 |
let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
|
wenzelm@22228
|
704 |
in
|
wenzelm@22228
|
705 |
issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
|
wenzelm@22228
|
706 |
name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
|
wenzelm@22228
|
707 |
ids=thyrefs}], fileurls=[]})
|
wenzelm@22228
|
708 |
end
|
aspinall@22159
|
709 |
|
wenzelm@22228
|
710 |
fun thmrefs thmname =
|
wenzelm@22228
|
711 |
let
|
wenzelm@22228
|
712 |
(* TODO: interim: this is probably not right.
|
wenzelm@22228
|
713 |
What we want is mapping onto simple PGIP name/context model. *)
|
wenzelm@22228
|
714 |
val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
|
wenzelm@22228
|
715 |
val thy = Context.theory_of_proof ctx
|
wenzelm@22228
|
716 |
val ths = [PureThy.get_thm thy (PureThy.Name thmname)]
|
wenzelm@22228
|
717 |
val deps = filter_out (equal "")
|
wenzelm@22228
|
718 |
(Symtab.keys (fold Proofterm.thms_of_proof
|
wenzelm@22228
|
719 |
(map Thm.proof_of ths) Symtab.empty))
|
wenzelm@22228
|
720 |
in
|
wenzelm@22228
|
721 |
if null deps then ()
|
wenzelm@22228
|
722 |
else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
|
wenzelm@22228
|
723 |
objtype=SOME PgipTypes.ObjTheorem,
|
wenzelm@22228
|
724 |
idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
|
wenzelm@22228
|
725 |
ids=deps}], fileurls=[]})
|
wenzelm@22228
|
726 |
end
|
aspinall@22159
|
727 |
in
|
aspinall@22159
|
728 |
case (url,thyname,objtype,name) of
|
wenzelm@22228
|
729 |
(SOME file, NONE, _, _) => filerefs file
|
wenzelm@22228
|
730 |
| (_,SOME thy,_,_) => thyrefs thy
|
wenzelm@22228
|
731 |
| (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
|
aspinall@22159
|
732 |
| _ => error ("Unimplemented/invalid case of <askrefs>")
|
aspinall@22159
|
733 |
end
|
aspinall@22159
|
734 |
|
aspinall@22159
|
735 |
|
aspinall@22159
|
736 |
|
wenzelm@21940
|
737 |
fun showid (Showid vs) =
|
aspinall@21637
|
738 |
let
|
wenzelm@21940
|
739 |
val thyname = #thyname vs
|
wenzelm@21940
|
740 |
val objtype = #objtype vs
|
wenzelm@21940
|
741 |
val name = #name vs
|
aspinall@22337
|
742 |
|
wenzelm@21940
|
743 |
val topthy = Toplevel.theory_of o Toplevel.get_state
|
aspinall@21637
|
744 |
|
wenzelm@22590
|
745 |
fun splitthy id =
|
wenzelm@22590
|
746 |
let val comps = NameSpace.explode id
|
wenzelm@22590
|
747 |
in case comps of
|
wenzelm@22590
|
748 |
(thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
|
wenzelm@22590
|
749 |
| [plainid] => (topthy(),plainid)
|
wenzelm@22590
|
750 |
| _ => raise Toplevel.UNDEF (* assert false *)
|
wenzelm@22590
|
751 |
end
|
wenzelm@22590
|
752 |
|
aspinall@21637
|
753 |
|
aspinall@22337
|
754 |
fun idvalue strings =
|
aspinall@22337
|
755 |
issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
|
aspinall@23759
|
756 |
text=[XML.Elem("pgml",[],
|
wenzelm@23723
|
757 |
map XML.Output strings)] })
|
aspinall@22337
|
758 |
|
wenzelm@22590
|
759 |
fun string_of_thm th = Output.output
|
wenzelm@22590
|
760 |
(Pretty.string_of
|
wenzelm@22590
|
761 |
(Display.pretty_thm_aux
|
wenzelm@22590
|
762 |
(Sign.pp (Thm.theory_of_thm th))
|
wenzelm@22590
|
763 |
false (* quote *)
|
wenzelm@22590
|
764 |
false (* show hyps *)
|
wenzelm@22590
|
765 |
[] (* asms *)
|
wenzelm@22590
|
766 |
th))
|
aspinall@22337
|
767 |
|
aspinall@22337
|
768 |
fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
|
aspinall@22337
|
769 |
|
wenzelm@22590
|
770 |
val string_of_thy = Output.output o
|
wenzelm@22590
|
771 |
Pretty.string_of o (ProofDisplay.pretty_full_theory false)
|
wenzelm@21940
|
772 |
in
|
wenzelm@21940
|
773 |
case (thyname, objtype) of
|
aspinall@22337
|
774 |
(_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
|
aspinall@22337
|
775 |
| (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
|
aspinall@22337
|
776 |
| (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
|
wenzelm@21940
|
777 |
| (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
|
aspinall@21637
|
778 |
end
|
aspinall@21637
|
779 |
|
aspinall@21867
|
780 |
(*** Inspecting state ***)
|
aspinall@21867
|
781 |
|
wenzelm@21940
|
782 |
(* The file which is currently being processed interactively.
|
aspinall@21637
|
783 |
In the pre-PGIP code, this was informed to Isabelle and the theory loader
|
aspinall@21637
|
784 |
on completion, but that allows for circularity in case we read
|
aspinall@21637
|
785 |
ourselves. So PGIP opens the filename at the start of a script.
|
aspinall@21637
|
786 |
We ought to prevent problems by modifying the theory loader to know
|
wenzelm@21940
|
787 |
about this special status, but for now we just keep a local reference.
|
wenzelm@21940
|
788 |
*)
|
aspinall@21637
|
789 |
|
aspinall@21637
|
790 |
val currently_open_file = ref (NONE : pgipurl option)
|
aspinall@21637
|
791 |
|
aspinall@22163
|
792 |
fun get_currently_open_file () = ! currently_open_file;
|
aspinall@22163
|
793 |
|
wenzelm@23834
|
794 |
fun askguise _ =
|
aspinall@21637
|
795 |
(* The "guise" is the PGIP abstraction of the prover's state.
|
aspinall@21637
|
796 |
The <informguise> message is merely used for consistency checking. *)
|
wenzelm@21940
|
797 |
let
|
wenzelm@21940
|
798 |
val openfile = !currently_open_file
|
aspinall@21637
|
799 |
|
wenzelm@21940
|
800 |
val topthy = Toplevel.theory_of o Toplevel.get_state
|
wenzelm@21940
|
801 |
val topthy_name = Context.theory_name o topthy
|
aspinall@21637
|
802 |
|
wenzelm@21940
|
803 |
val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
|
aspinall@21637
|
804 |
|
wenzelm@21940
|
805 |
fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
|
wenzelm@21940
|
806 |
val openproofpos = topproofpos()
|
aspinall@21637
|
807 |
in
|
aspinall@21637
|
808 |
issue_pgip (Informguise { file = openfile,
|
wenzelm@21940
|
809 |
theory = opentheory,
|
wenzelm@21940
|
810 |
(* would be nice to get thm name... *)
|
wenzelm@21940
|
811 |
theorem = NONE,
|
wenzelm@21940
|
812 |
proofpos = openproofpos })
|
aspinall@21637
|
813 |
end
|
aspinall@21637
|
814 |
|
haftmann@21902
|
815 |
fun parsescript (Parsescript vs) =
|
aspinall@21637
|
816 |
let
|
wenzelm@21940
|
817 |
val text = #text vs
|
wenzelm@21940
|
818 |
val systemdata = #systemdata vs
|
wenzelm@21940
|
819 |
val location = #location vs (* TODO: extract position *)
|
aspinall@21637
|
820 |
|
aspinall@21867
|
821 |
val _ = start_delay_msgs () (* gather parsing errs/warns *)
|
wenzelm@23801
|
822 |
val doc = OldPgipParser.pgip_parser text
|
aspinall@23840
|
823 |
(* not yet working: PgipParser.pgip_parser Position.none text *)
|
aspinall@21637
|
824 |
val errs = end_delayed_msgs ()
|
aspinall@21637
|
825 |
|
wenzelm@21940
|
826 |
val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
|
wenzelm@21940
|
827 |
val locattrs = PgipTypes.attrs_of_location location
|
aspinall@21637
|
828 |
in
|
aspinall@21637
|
829 |
issue_pgip (Parseresult { attrs= sysattrs@locattrs,
|
wenzelm@21940
|
830 |
doc = doc,
|
wenzelm@21940
|
831 |
errs = map PgipOutput.output errs })
|
aspinall@21637
|
832 |
end
|
aspinall@21637
|
833 |
|
wenzelm@23834
|
834 |
fun showproofstate _ = isarcmd "pr"
|
aspinall@21637
|
835 |
|
wenzelm@23834
|
836 |
fun showctxt _ = isarcmd "print_context"
|
aspinall@21637
|
837 |
|
haftmann@21902
|
838 |
fun searchtheorems (Searchtheorems vs) =
|
wenzelm@21940
|
839 |
let
|
wenzelm@21940
|
840 |
val arg = #arg vs
|
aspinall@21637
|
841 |
in
|
wenzelm@21969
|
842 |
isarcmd ("find_theorems " ^ arg)
|
aspinall@21637
|
843 |
end
|
aspinall@21637
|
844 |
|
wenzelm@21940
|
845 |
fun setlinewidth (Setlinewidth vs) =
|
wenzelm@21940
|
846 |
let
|
wenzelm@21940
|
847 |
val width = #width vs
|
aspinall@21637
|
848 |
in
|
wenzelm@21940
|
849 |
isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
|
aspinall@21637
|
850 |
end
|
aspinall@21637
|
851 |
|
haftmann@21902
|
852 |
fun viewdoc (Viewdoc vs) =
|
wenzelm@21940
|
853 |
let
|
wenzelm@21940
|
854 |
val arg = #arg vs
|
wenzelm@21940
|
855 |
in
|
wenzelm@21940
|
856 |
isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *)
|
aspinall@21637
|
857 |
end
|
aspinall@21637
|
858 |
|
aspinall@21867
|
859 |
(*** Theory ***)
|
aspinall@21867
|
860 |
|
haftmann@21902
|
861 |
fun doitem (Doitem vs) =
|
aspinall@21637
|
862 |
let
|
wenzelm@21940
|
863 |
val text = #text vs
|
aspinall@21637
|
864 |
in
|
wenzelm@21940
|
865 |
isarcmd text
|
aspinall@21637
|
866 |
end
|
aspinall@21637
|
867 |
|
wenzelm@23834
|
868 |
fun undoitem _ =
|
aspinall@21972
|
869 |
isarcmd "undo"
|
aspinall@21637
|
870 |
|
wenzelm@23834
|
871 |
fun redoitem _ =
|
aspinall@21972
|
872 |
isarcmd "redo"
|
aspinall@21637
|
873 |
|
wenzelm@23834
|
874 |
fun aborttheory _ =
|
aspinall@21972
|
875 |
isarcmd "kill" (* was: "init_toplevel" *)
|
aspinall@21637
|
876 |
|
haftmann@21902
|
877 |
fun retracttheory (Retracttheory vs) =
|
wenzelm@21940
|
878 |
let
|
wenzelm@21940
|
879 |
val thyname = #thyname vs
|
aspinall@21637
|
880 |
in
|
wenzelm@21940
|
881 |
isarcmd ("kill_thy " ^ quote thyname)
|
aspinall@21637
|
882 |
end
|
aspinall@21637
|
883 |
|
aspinall@21867
|
884 |
|
aspinall@21867
|
885 |
(*** Files ***)
|
aspinall@21867
|
886 |
|
aspinall@21867
|
887 |
(* Path management: we allow theory files to have dependencies in
|
aspinall@21867
|
888 |
their own directory, but when we change directory for a new file we
|
aspinall@21867
|
889 |
remove the path. Leaving it there can cause confusion with
|
aspinall@21867
|
890 |
difference in batch mode.
|
wenzelm@21940
|
891 |
NB: PGIP does not assume that the prover has a load path.
|
aspinall@21867
|
892 |
*)
|
aspinall@21867
|
893 |
|
aspinall@21867
|
894 |
local
|
aspinall@21867
|
895 |
val current_working_dir = ref (NONE : string option)
|
aspinall@21867
|
896 |
in
|
wenzelm@21940
|
897 |
fun changecwd_dir newdirpath =
|
wenzelm@21940
|
898 |
let
|
aspinall@21867
|
899 |
val newdir = File.platform_path newdirpath
|
wenzelm@21940
|
900 |
in
|
aspinall@21867
|
901 |
(case (!current_working_dir) of
|
aspinall@21867
|
902 |
NONE => ()
|
aspinall@21867
|
903 |
| SOME dir => ThyLoad.del_path dir;
|
aspinall@21867
|
904 |
ThyLoad.add_path newdir;
|
aspinall@21867
|
905 |
current_working_dir := SOME newdir)
|
aspinall@21867
|
906 |
end
|
aspinall@21867
|
907 |
end
|
aspinall@21867
|
908 |
|
wenzelm@21940
|
909 |
fun changecwd (Changecwd vs) =
|
wenzelm@21940
|
910 |
let
|
wenzelm@21940
|
911 |
val url = #url vs
|
wenzelm@21940
|
912 |
val newdir = PgipTypes.path_of_pgipurl url
|
aspinall@21867
|
913 |
in
|
wenzelm@21940
|
914 |
changecwd_dir url
|
aspinall@21867
|
915 |
end
|
aspinall@21867
|
916 |
|
haftmann@21902
|
917 |
fun openfile (Openfile vs) =
|
wenzelm@21940
|
918 |
let
|
aspinall@21867
|
919 |
val url = #url vs
|
aspinall@21867
|
920 |
val filepath = PgipTypes.path_of_pgipurl url
|
aspinall@21867
|
921 |
val filedir = Path.dir filepath
|
aspinall@21867
|
922 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base
|
aspinall@21867
|
923 |
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
|
aspinall@21867
|
924 |
in
|
aspinall@21867
|
925 |
case !currently_open_file of
|
aspinall@22028
|
926 |
SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
|
wenzelm@22228
|
927 |
PgipTypes.string_of_pgipurl url)
|
aspinall@21867
|
928 |
| NONE => (openfile_retract filepath;
|
wenzelm@21940
|
929 |
changecwd_dir filedir;
|
wenzelm@22228
|
930 |
priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
|
wenzelm@21940
|
931 |
currently_open_file := SOME url)
|
aspinall@21867
|
932 |
end
|
aspinall@21867
|
933 |
|
wenzelm@23834
|
934 |
fun closefile _ =
|
aspinall@21867
|
935 |
case !currently_open_file of
|
aspinall@22042
|
936 |
SOME f => (proper_inform_file_processed f (Isar.state());
|
wenzelm@22228
|
937 |
priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
|
aspinall@21867
|
938 |
currently_open_file := NONE)
|
aspinall@21867
|
939 |
| NONE => raise PGIP ("<closefile> when no file is open!")
|
aspinall@21867
|
940 |
|
wenzelm@21940
|
941 |
fun loadfile (Loadfile vs) =
|
wenzelm@21940
|
942 |
let
|
wenzelm@21940
|
943 |
val url = #url vs
|
wenzelm@21940
|
944 |
in
|
aspinall@22171
|
945 |
(* da: this doesn't seem to cause a problem, batch loading uses
|
aspinall@22171
|
946 |
a different state context. Of course confusion is still possible,
|
aspinall@22171
|
947 |
e.g. file loaded depends on open file which is not yet saved. *)
|
aspinall@22171
|
948 |
(* case !currently_open_file of
|
aspinall@22028
|
949 |
SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
|
wenzelm@22228
|
950 |
PgipTypes.string_of_pgipurl url)
|
aspinall@22171
|
951 |
| NONE => *)
|
wenzelm@22228
|
952 |
use_thy_or_ml_file (File.platform_path url)
|
aspinall@21637
|
953 |
end
|
aspinall@21637
|
954 |
|
wenzelm@23834
|
955 |
fun abortfile _ =
|
aspinall@21637
|
956 |
case !currently_open_file of
|
aspinall@21637
|
957 |
SOME f => (isarcmd "init_toplevel";
|
wenzelm@22228
|
958 |
priority ("Aborted working in file: " ^
|
wenzelm@22228
|
959 |
PgipTypes.string_of_pgipurl f);
|
wenzelm@21940
|
960 |
currently_open_file := NONE)
|
aspinall@21637
|
961 |
| NONE => raise PGIP ("<abortfile> when no file is open!")
|
aspinall@21637
|
962 |
|
wenzelm@21940
|
963 |
fun retractfile (Retractfile vs) =
|
wenzelm@21940
|
964 |
let
|
wenzelm@21940
|
965 |
val url = #url vs
|
aspinall@21637
|
966 |
in
|
wenzelm@21940
|
967 |
case !currently_open_file of
|
aspinall@21637
|
968 |
SOME f => raise PGIP ("<retractfile> when a file is open!")
|
aspinall@22028
|
969 |
| NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
|
wenzelm@22228
|
970 |
(* TODO: next should be in thy loader, here just for testing *)
|
wenzelm@22228
|
971 |
let
|
wenzelm@22228
|
972 |
val name = thy_name url
|
wenzelm@22228
|
973 |
in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
|
wenzelm@22228
|
974 |
inform_file_retracted url)
|
aspinall@21637
|
975 |
end
|
aspinall@21637
|
976 |
|
aspinall@21637
|
977 |
|
aspinall@21867
|
978 |
(*** System ***)
|
aspinall@21637
|
979 |
|
haftmann@21902
|
980 |
fun systemcmd (Systemcmd vs) =
|
wenzelm@21940
|
981 |
let
|
aspinall@21637
|
982 |
val arg = #arg vs
|
aspinall@21637
|
983 |
in
|
aspinall@21637
|
984 |
isarcmd arg
|
aspinall@21637
|
985 |
end
|
aspinall@21637
|
986 |
|
aspinall@21637
|
987 |
exception PGIP_QUIT;
|
wenzelm@23834
|
988 |
fun quitpgip _ = raise PGIP_QUIT
|
aspinall@21637
|
989 |
|
haftmann@21902
|
990 |
fun process_input inp = case inp
|
haftmann@21902
|
991 |
of Pgip.Askpgip _ => askpgip inp
|
haftmann@21902
|
992 |
| Pgip.Askpgml _ => askpgml inp
|
wenzelm@21940
|
993 |
| Pgip.Askprefs _ => askprefs inp
|
haftmann@21902
|
994 |
| Pgip.Askconfig _ => askconfig inp
|
haftmann@21902
|
995 |
| Pgip.Getpref _ => getpref inp
|
haftmann@21902
|
996 |
| Pgip.Setpref _ => setpref inp
|
haftmann@21902
|
997 |
| Pgip.Proverinit _ => proverinit inp
|
haftmann@21902
|
998 |
| Pgip.Proverexit _ => proverexit inp
|
aspinall@22408
|
999 |
| Pgip.Setproverflag _ => setproverflag inp
|
haftmann@21902
|
1000 |
| Pgip.Dostep _ => dostep inp
|
haftmann@21902
|
1001 |
| Pgip.Undostep _ => undostep inp
|
haftmann@21902
|
1002 |
| Pgip.Redostep _ => redostep inp
|
aspinall@23435
|
1003 |
| Pgip.Forget _ => error "<forget> not implemented by Isabelle"
|
aspinall@23435
|
1004 |
| Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
|
haftmann@21902
|
1005 |
| Pgip.Abortgoal _ => abortgoal inp
|
haftmann@21902
|
1006 |
| Pgip.Askids _ => askids inp
|
aspinall@22159
|
1007 |
| Pgip.Askrefs _ => askrefs inp
|
haftmann@21902
|
1008 |
| Pgip.Showid _ => showid inp
|
haftmann@21902
|
1009 |
| Pgip.Askguise _ => askguise inp
|
haftmann@21902
|
1010 |
| Pgip.Parsescript _ => parsescript inp
|
haftmann@21902
|
1011 |
| Pgip.Showproofstate _ => showproofstate inp
|
haftmann@21902
|
1012 |
| Pgip.Showctxt _ => showctxt inp
|
haftmann@21902
|
1013 |
| Pgip.Searchtheorems _ => searchtheorems inp
|
haftmann@21902
|
1014 |
| Pgip.Setlinewidth _ => setlinewidth inp
|
haftmann@21902
|
1015 |
| Pgip.Viewdoc _ => viewdoc inp
|
haftmann@21902
|
1016 |
| Pgip.Doitem _ => doitem inp
|
haftmann@21902
|
1017 |
| Pgip.Undoitem _ => undoitem inp
|
haftmann@21902
|
1018 |
| Pgip.Redoitem _ => redoitem inp
|
haftmann@21902
|
1019 |
| Pgip.Aborttheory _ => aborttheory inp
|
haftmann@21902
|
1020 |
| Pgip.Retracttheory _ => retracttheory inp
|
haftmann@21902
|
1021 |
| Pgip.Loadfile _ => loadfile inp
|
haftmann@21902
|
1022 |
| Pgip.Openfile _ => openfile inp
|
haftmann@21902
|
1023 |
| Pgip.Closefile _ => closefile inp
|
haftmann@21902
|
1024 |
| Pgip.Abortfile _ => abortfile inp
|
haftmann@21902
|
1025 |
| Pgip.Retractfile _ => retractfile inp
|
haftmann@21902
|
1026 |
| Pgip.Changecwd _ => changecwd inp
|
haftmann@21902
|
1027 |
| Pgip.Systemcmd _ => systemcmd inp
|
haftmann@21902
|
1028 |
| Pgip.Quitpgip _ => quitpgip inp
|
aspinall@21637
|
1029 |
|
aspinall@21637
|
1030 |
|
wenzelm@21940
|
1031 |
fun process_pgip_element pgipxml =
|
aspinall@21637
|
1032 |
case pgipxml of
|
wenzelm@21969
|
1033 |
xml as (XML.Elem elem) =>
|
wenzelm@21940
|
1034 |
(case Pgip.input elem of
|
wenzelm@21940
|
1035 |
NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
|
wenzelm@21940
|
1036 |
(XML.string_of_tree xml))
|
wenzelm@21940
|
1037 |
| SOME inp => (process_input inp)) (* errors later; packet discarded *)
|
wenzelm@21969
|
1038 |
| XML.Text t => ignored_text_warning t
|
wenzelm@23723
|
1039 |
| XML.Output t => ignored_text_warning t
|
aspinall@21637
|
1040 |
and ignored_text_warning t =
|
wenzelm@21940
|
1041 |
if size (Symbol.strip_blanks t) > 0 then
|
wenzelm@21940
|
1042 |
warning ("Ignored text in PGIP packet: \n" ^ t)
|
aspinall@21637
|
1043 |
else ()
|
aspinall@21637
|
1044 |
|
aspinall@21637
|
1045 |
fun process_pgip_tree xml =
|
aspinall@21637
|
1046 |
(pgip_refid := NONE;
|
aspinall@21637
|
1047 |
pgip_refseq := NONE;
|
aspinall@21637
|
1048 |
(case xml of
|
aspinall@21637
|
1049 |
XML.Elem ("pgip", attrs, pgips) =>
|
aspinall@21637
|
1050 |
(let
|
aspinall@21637
|
1051 |
val class = PgipTypes.get_attr "class" attrs
|
aspinall@21637
|
1052 |
val dest = PgipTypes.get_attr_opt "destid" attrs
|
wenzelm@21940
|
1053 |
val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
|
aspinall@21637
|
1054 |
(* Respond to prover broadcasts, or messages for us. Ignore rest *)
|
wenzelm@21940
|
1055 |
val processit =
|
wenzelm@21940
|
1056 |
case dest of
|
aspinall@21637
|
1057 |
NONE => class = "pa"
|
wenzelm@21940
|
1058 |
| SOME id => matching_pgip_id id
|
wenzelm@21940
|
1059 |
in if processit then
|
wenzelm@21940
|
1060 |
(pgip_refid := PgipTypes.get_attr_opt "id" attrs;
|
wenzelm@21940
|
1061 |
pgip_refseq := SOME seq;
|
wenzelm@21940
|
1062 |
List.app process_pgip_element pgips;
|
wenzelm@21940
|
1063 |
(* return true to indicate <ready/> *)
|
wenzelm@21940
|
1064 |
true)
|
wenzelm@21940
|
1065 |
else
|
wenzelm@21940
|
1066 |
(* no response to ignored messages. *)
|
wenzelm@21940
|
1067 |
false
|
aspinall@21637
|
1068 |
end)
|
aspinall@21637
|
1069 |
| _ => raise PGIP "Invalid PGIP packet received")
|
aspinall@21637
|
1070 |
handle PGIP msg =>
|
aspinall@21637
|
1071 |
(Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
|
wenzelm@21940
|
1072 |
(XML.string_of_tree xml));
|
wenzelm@21940
|
1073 |
true))
|
aspinall@21637
|
1074 |
|
aspinall@21649
|
1075 |
(* External input *)
|
aspinall@21649
|
1076 |
|
aspinall@21649
|
1077 |
val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
|
aspinall@21637
|
1078 |
|
aspinall@21637
|
1079 |
(* PGIP loop: process PGIP input only *)
|
aspinall@21637
|
1080 |
|
aspinall@21637
|
1081 |
local
|
aspinall@21637
|
1082 |
|
aspinall@21637
|
1083 |
exception XML_PARSE
|
aspinall@21637
|
1084 |
|
aspinall@21637
|
1085 |
fun loop ready src =
|
aspinall@21637
|
1086 |
let
|
aspinall@21637
|
1087 |
val _ = if ready then issue_pgip (Ready ()) else ()
|
wenzelm@21969
|
1088 |
val pgipo =
|
wenzelm@21969
|
1089 |
(case try Source.get_single src of
|
wenzelm@21969
|
1090 |
SOME pgipo => pgipo
|
wenzelm@21969
|
1091 |
| NONE => raise XML_PARSE)
|
aspinall@21637
|
1092 |
in
|
aspinall@21637
|
1093 |
case pgipo of
|
aspinall@21637
|
1094 |
NONE => ()
|
aspinall@21637
|
1095 |
| SOME (pgip,src') =>
|
aspinall@21637
|
1096 |
let
|
wenzelm@21940
|
1097 |
val ready' = (process_pgip_tree pgip)
|
aspinall@22337
|
1098 |
handle PGIP_QUIT => raise PGIP_QUIT
|
wenzelm@22590
|
1099 |
| e => (handler (e,SOME src'); true)
|
aspinall@21637
|
1100 |
in
|
aspinall@21637
|
1101 |
loop ready' src'
|
aspinall@21637
|
1102 |
end
|
aspinall@21637
|
1103 |
end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
|
aspinall@21637
|
1104 |
|
aspinall@21637
|
1105 |
and handler (e,srco) =
|
aspinall@21637
|
1106 |
case (e,srco) of
|
aspinall@21637
|
1107 |
(XML_PARSE,SOME src) =>
|
wenzelm@22699
|
1108 |
panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
|
wenzelm@21940
|
1109 |
| (Interrupt,SOME src) =>
|
wenzelm@21940
|
1110 |
(Output.error_msg "Interrupt during PGIP processing"; loop true src)
|
wenzelm@21940
|
1111 |
| (Toplevel.UNDEF,SOME src) =>
|
wenzelm@21940
|
1112 |
(Output.error_msg "No working context defined"; loop true src)
|
wenzelm@21940
|
1113 |
| (e,SOME src) =>
|
wenzelm@21940
|
1114 |
(Output.error_msg (Toplevel.exn_message e); loop true src)
|
aspinall@22337
|
1115 |
| (PGIP_QUIT,_) => ()
|
aspinall@21637
|
1116 |
| (_,NONE) => ()
|
aspinall@21637
|
1117 |
in
|
aspinall@21637
|
1118 |
(* TODO: add socket interface *)
|
aspinall@21637
|
1119 |
|
aspinall@21637
|
1120 |
val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
|
aspinall@21637
|
1121 |
|
aspinall@21637
|
1122 |
val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
|
aspinall@21637
|
1123 |
|
aspinall@21637
|
1124 |
fun pgip_toplevel x = loop true x
|
aspinall@21637
|
1125 |
end
|
aspinall@21637
|
1126 |
|
aspinall@21637
|
1127 |
|
aspinall@21972
|
1128 |
local
|
aspinall@21972
|
1129 |
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
|
aspinall@21637
|
1130 |
|
wenzelm@22014
|
1131 |
val process_pgipP =
|
aspinall@21972
|
1132 |
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
|
aspinall@21972
|
1133 |
(OuterParse.text >> (Toplevel.no_timing oo
|
aspinall@21649
|
1134 |
(fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
|
aspinall@21637
|
1135 |
|
aspinall@21972
|
1136 |
in
|
aspinall@21637
|
1137 |
|
aspinall@21972
|
1138 |
fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
|
aspinall@21972
|
1139 |
|
aspinall@21972
|
1140 |
end
|
aspinall@21972
|
1141 |
|
aspinall@21637
|
1142 |
|
aspinall@21637
|
1143 |
|
aspinall@21637
|
1144 |
(* init *)
|
aspinall@21637
|
1145 |
|
aspinall@21637
|
1146 |
val initialized = ref false;
|
aspinall@21637
|
1147 |
|
wenzelm@22699
|
1148 |
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
|
wenzelm@21969
|
1149 |
| init_pgip true =
|
wenzelm@21969
|
1150 |
(! initialized orelse
|
wenzelm@22590
|
1151 |
(Output.no_warnings init_outer_syntax ();
|
wenzelm@23801
|
1152 |
OldPgipParser.init ();
|
wenzelm@22228
|
1153 |
setup_preferences_tweak ();
|
wenzelm@22590
|
1154 |
setup_proofgeneral_output ();
|
wenzelm@21969
|
1155 |
setup_messages ();
|
wenzelm@21969
|
1156 |
setup_thy_loader ();
|
wenzelm@21969
|
1157 |
setup_present_hook ();
|
wenzelm@21969
|
1158 |
init_pgip_session_id ();
|
wenzelm@21969
|
1159 |
welcome ();
|
wenzelm@21969
|
1160 |
set initialized);
|
wenzelm@21969
|
1161 |
sync_thy_loader ();
|
wenzelm@21969
|
1162 |
change print_mode (cons proof_generalN o remove (op =) proof_generalN);
|
wenzelm@21969
|
1163 |
pgip_toplevel tty_src);
|
aspinall@21637
|
1164 |
|
aspinall@21649
|
1165 |
|
aspinall@21649
|
1166 |
|
aspinall@21649
|
1167 |
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
|
aspinall@21649
|
1168 |
|
aspinall@21649
|
1169 |
local
|
wenzelm@22590
|
1170 |
val pgip_output_channel = ref Output.writeln_default
|
aspinall@21649
|
1171 |
in
|
aspinall@21649
|
1172 |
|
aspinall@21649
|
1173 |
(* Set recipient for PGIP results *)
|
aspinall@21649
|
1174 |
fun init_pgip_channel writefn =
|
wenzelm@21940
|
1175 |
(init_pgip_session_id();
|
wenzelm@21940
|
1176 |
pgip_output_channel := writefn)
|
aspinall@21649
|
1177 |
|
wenzelm@21940
|
1178 |
(* Process a PGIP command.
|
wenzelm@21940
|
1179 |
This works for preferences but not generally guaranteed
|
aspinall@21649
|
1180 |
because we haven't done full setup here (e.g., no pgml mode) *)
|
aspinall@21649
|
1181 |
fun process_pgip str =
|
aspinall@21649
|
1182 |
setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
|
aspinall@21649
|
1183 |
|
aspinall@21649
|
1184 |
end
|
aspinall@21637
|
1185 |
|
aspinall@21637
|
1186 |
end;
|