author | wenzelm |
Mon, 10 May 2004 19:25:42 +0200 | |
changeset 14725 | 2ed5b960c6b1 |
parent 14707 | 2d6350d7b9b7 |
child 14827 | d973e7f820cb |
permissions | -rw-r--r-- |
12780 | 1 |
(* Title: Pure/proof_general.ML |
12778 | 2 |
ID: $Id$ |
14675 | 3 |
Author: David Aspinall and Markus Wenzel |
12778 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
||
14566 | 6 |
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk). |
12778 | 7 |
*) |
8 |
||
9 |
signature PROOF_GENERAL = |
|
10 |
sig |
|
11 |
val setup: (theory -> theory) list |
|
12 |
val update_thy_only: string -> unit |
|
13 |
val try_update_thy_only: string -> unit |
|
13391 | 14 |
val inform_file_retracted: string -> unit |
12778 | 15 |
val inform_file_processed: string -> unit |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
16 |
val options: (string * (string * (string * (unit -> string) * (string -> unit)))) list ref |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
17 |
val process_pgip: string -> unit |
12778 | 18 |
val thms_containing: string list -> unit |
19 |
val help: unit -> unit |
|
20 |
val show_context: unit -> theory |
|
21 |
val kill_goal: unit -> unit |
|
22 |
val repeat_undo: int -> unit |
|
23 |
val isa_restart: unit -> unit |
|
12833 | 24 |
val full_proofs: bool -> unit |
12778 | 25 |
val init: bool -> unit |
26 |
val write_keywords: string -> unit |
|
27 |
end; |
|
28 |
||
29 |
structure ProofGeneral: PROOF_GENERAL = |
|
30 |
struct |
|
31 |
||
32 |
(* print modes *) |
|
33 |
||
34 |
val proof_generalN = "ProofGeneral"; |
|
35 |
val xsymbolsN = "xsymbols"; |
|
13538 | 36 |
val thm_depsN = "thm_deps"; |
12778 | 37 |
|
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
38 |
val pgml_version_supported = "1.0"; |
12778 | 39 |
val pgmlN = "PGML"; |
40 |
fun pgml () = pgmlN mem_string ! print_mode; |
|
41 |
||
42 |
||
43 |
(* text output *) |
|
44 |
||
45 |
local |
|
46 |
||
47 |
fun xsymbols_output s = |
|
48 |
if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then |
|
49 |
let val syms = Symbol.explode s |
|
14567 | 50 |
in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end |
12778 | 51 |
else (s, real (size s)); |
52 |
||
53 |
fun pgml_output (s, len) = |
|
54 |
if pgml () then (XML.text s, len) |
|
55 |
else (s, len); |
|
56 |
||
57 |
in |
|
58 |
||
59 |
fun setup_xsymbols_output () = |
|
60 |
Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent); |
|
61 |
||
62 |
end; |
|
63 |
||
64 |
||
65 |
(* token translations *) |
|
66 |
||
67 |
local |
|
68 |
||
69 |
val end_tag = oct_char "350"; |
|
70 |
val class_tag = ("class", oct_char "351"); |
|
71 |
val tfree_tag = ("tfree", oct_char "352"); |
|
72 |
val tvar_tag = ("tvar", oct_char "353"); |
|
73 |
val free_tag = ("free", oct_char "354"); |
|
74 |
val bound_tag = ("bound", oct_char "355"); |
|
75 |
val var_tag = ("var", oct_char "356"); |
|
76 |
val skolem_tag = ("skolem", oct_char "357"); |
|
77 |
||
78 |
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; |
|
79 |
||
80 |
fun tagit (kind, bg_tag) x = |
|
81 |
(if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag, |
|
82 |
real (Symbol.length (Symbol.explode x))); |
|
83 |
||
84 |
fun free_or_skolem x = |
|
85 |
(case try Syntax.dest_skolem x of |
|
86 |
None => tagit free_tag x |
|
87 |
| Some x' => tagit skolem_tag x'); |
|
88 |
||
89 |
fun var_or_skolem s = |
|
90 |
(case Syntax.read_var s of |
|
91 |
Var ((x, i), _) => |
|
92 |
(case try Syntax.dest_skolem x of |
|
93 |
None => tagit var_tag s |
|
94 |
| Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i))) |
|
95 |
| _ => tagit var_tag s); |
|
96 |
||
97 |
val proof_general_trans = |
|
98 |
Syntax.tokentrans_mode proof_generalN |
|
99 |
[("class", tagit class_tag), |
|
100 |
("tfree", tagit tfree_tag), |
|
101 |
("tvar", tagit tvar_tag), |
|
102 |
("free", free_or_skolem), |
|
103 |
("bound", tagit bound_tag), |
|
104 |
("var", var_or_skolem)]; |
|
105 |
||
106 |
in val setup = [Theory.add_tokentrfuns proof_general_trans] end; |
|
107 |
||
108 |
||
109 |
(* messages and notification *) |
|
110 |
||
111 |
local |
|
112 |
||
113 |
fun decorated_output bg en prfx = |
|
114 |
writeln_default o enclose bg en o prefix_lines prfx; |
|
115 |
||
116 |
fun message kind bg en prfx s = |
|
117 |
if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s]) |
|
118 |
else decorated_output bg en prfx s; |
|
119 |
||
13526 | 120 |
in |
12778 | 121 |
|
13526 | 122 |
val notify = message "notify" (oct_char "360") (oct_char "361") ""; |
12778 | 123 |
|
124 |
fun setup_messages () = |
|
125 |
(writeln_fn := message "output" "" "" ""; |
|
126 |
priority_fn := message "information" (oct_char "360") (oct_char "361") ""; |
|
127 |
tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") ""; |
|
128 |
warning_fn := message "warning" (oct_char "362") (oct_char "363") "### "; |
|
129 |
error_fn := message "error" (oct_char "364") (oct_char "365") "*** "); |
|
130 |
||
131 |
fun tell_clear_goals () = notify "Proof General, please clear the goals buffer."; |
|
132 |
fun tell_clear_response () = notify "Proof General, please clear the response buffer."; |
|
133 |
fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path)); |
|
134 |
||
135 |
end; |
|
136 |
||
137 |
||
138 |
(* theory / proof state output *) |
|
139 |
||
140 |
local |
|
141 |
||
142 |
fun tmp_markers f = |
|
143 |
setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f (); |
|
144 |
||
145 |
fun statedisplay prts = |
|
146 |
writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]); |
|
147 |
||
148 |
fun print_current_goals n m st = |
|
149 |
if pgml () then statedisplay (Display.pretty_current_goals n m st) |
|
150 |
else tmp_markers (fn () => Display.print_current_goals_default n m st); |
|
151 |
||
152 |
fun print_state b st = |
|
153 |
if pgml () then statedisplay (Toplevel.pretty_state b st) |
|
154 |
else tmp_markers (fn () => Toplevel.print_state_default b st); |
|
155 |
||
156 |
in |
|
157 |
||
158 |
fun setup_state () = |
|
159 |
(Display.print_current_goals_fn := print_current_goals; |
|
160 |
Toplevel.print_state_fn := print_state; |
|
161 |
Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default)); |
|
162 |
||
163 |
end; |
|
164 |
||
165 |
||
13538 | 166 |
(* theorem dependency output *) |
13526 | 167 |
|
168 |
local |
|
169 |
||
13545 | 170 |
val spaces_quote = space_implode " " o map quote; |
171 |
||
13526 | 172 |
fun tell_thm_deps ths = |
13538 | 173 |
conditional (thm_depsN mem_string ! print_mode) (fn () => |
174 |
let |
|
13545 | 175 |
val names = map Thm.name_of_thm ths \ ""; |
176 |
val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof) |
|
177 |
(Symtab.empty, map Thm.proof_of ths)) \ ""; |
|
13538 | 178 |
in |
13545 | 179 |
if null names orelse null deps then () |
180 |
else notify ("Proof General, theorem dependencies of " ^ spaces_quote names ^ " are " |
|
181 |
^ spaces_quote deps) |
|
13538 | 182 |
end); |
13526 | 183 |
|
184 |
in |
|
185 |
||
186 |
fun setup_present_hook () = |
|
187 |
Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res))); |
|
188 |
||
189 |
end; |
|
190 |
||
191 |
||
12778 | 192 |
(* theory loader actions *) |
193 |
||
194 |
local |
|
195 |
||
196 |
fun add_master_files name files = |
|
197 |
let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name] |
|
198 |
in masters @ gen_rems (op = o pairself Path.base) (files, masters) end; |
|
199 |
||
200 |
fun trace_action action name = |
|
201 |
if action = ThyInfo.Update then |
|
202 |
seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name) |
|
203 |
else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then |
|
204 |
seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name)) |
|
205 |
else (); |
|
206 |
||
207 |
in |
|
208 |
fun setup_thy_loader () = ThyInfo.add_hook trace_action; |
|
209 |
fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ()); |
|
210 |
end; |
|
211 |
||
212 |
||
213 |
(* prepare theory context *) |
|
214 |
||
215 |
val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack; |
|
216 |
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only; |
|
217 |
||
218 |
fun which_context () = |
|
219 |
(case Context.get_context () of |
|
220 |
Some thy => " Using current (dynamic!) one: " ^ |
|
221 |
(case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>") |
|
222 |
| None => ""); |
|
223 |
||
224 |
fun try_update_thy_only file = |
|
225 |
ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () => |
|
226 |
let val name = thy_name file in |
|
227 |
if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name |
|
228 |
else warning ("Unkown theory context of ML file." ^ which_context ()) |
|
229 |
end) (); |
|
230 |
||
231 |
||
232 |
(* get informed about files *) |
|
233 |
||
13391 | 234 |
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; |
235 |
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name; |
|
12778 | 236 |
|
237 |
fun proper_inform_file_processed file state = |
|
238 |
let val name = thy_name file in |
|
13391 | 239 |
ThyInfo.if_known_thy ThyInfo.touch_child_thys name; |
12778 | 240 |
if not (Toplevel.is_toplevel state) then |
241 |
warning ("Not at toplevel -- cannot register theory " ^ quote name) |
|
242 |
else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg => |
|
243 |
(warning msg; warning ("Failed to register theory " ^ quote name)) |
|
244 |
end; |
|
245 |
||
246 |
||
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
247 |
(* options *) |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
248 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
249 |
fun nat_option r = ("nat", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
250 |
(fn () => string_of_int (!r)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
251 |
(fn s => (case Syntax.read_nat s of |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
252 |
None => error "nat_option: illegal value" |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
253 |
| Some i => r := i))); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
254 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
255 |
fun bool_option r = ("boolean", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
256 |
(fn () => Bool.toString (!r)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
257 |
(fn "false" => r := false | "true" => r := true |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
258 |
| _ => error "bool_option: illegal value")); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
259 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
260 |
val proof_option = ("boolean", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
261 |
(fn () => Bool.toString (!proofs >= 2)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
262 |
(fn "false" => proofs := 1 | "true" => proofs := 2 |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
263 |
| _ => error "proof_option: illegal value")); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
264 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
265 |
val thm_deps_option = ("boolean", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
266 |
(fn () => Bool.toString ("thm_deps" mem !print_mode)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
267 |
(fn "false" => print_mode := Library.gen_rems (op =) (!print_mode, ["thm_deps"]) |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
268 |
| "true" => print_mode := (["thm_deps"] @ !print_mode) |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
269 |
| _ => error "thm_deps_option: illegal value")); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
270 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
271 |
val print_depth_option = ("nat", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
272 |
(fn () => "10"), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
273 |
(fn s => (case Syntax.read_nat s of |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
274 |
None => error "print_depth_option: illegal value" |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
275 |
| Some i => print_depth i))); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
276 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
277 |
val options = ref |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
278 |
[("show-types", ("Whether to show types in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
279 |
bool_option show_types)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
280 |
("show-sorts", ("Whether to show sorts in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
281 |
bool_option show_sorts)), |
14707 | 282 |
("show-structs", ("Whether to show implicit structures in Isabelle.", |
283 |
bool_option show_structs)), |
|
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
284 |
("show-consts", ("Whether to show types of consts in Isabelle goals.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
285 |
bool_option show_consts)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
286 |
("long-names", ("Whether to show fully qualified names in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
287 |
bool_option long_names)), |
13884 | 288 |
("show-brackets", ("Whether to show full bracketing in Isabelle.", |
289 |
bool_option show_brackets)), |
|
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
290 |
("eta-contract", ("Whether to print terms eta-contracted in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
291 |
bool_option Syntax.eta_contract)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
292 |
("trace-simplifier", ("Whether to trace the Simplifier in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
293 |
bool_option trace_simp)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
294 |
("trace-rules", ("Whether to trace the standard rules in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
295 |
bool_option trace_rules)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
296 |
("quick-and-dirty", ("Whether to take a few short cuts occasionally.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
297 |
bool_option quick_and_dirty)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
298 |
("full-proofs", ("Whether to record full proof objects internally.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
299 |
proof_option)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
300 |
("trace-unification", ("Whether to output error diagnostics during unification.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
301 |
bool_option Pattern.trace_unify_fail)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
302 |
("show-main-goal", ("Whether to show main goal.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
303 |
bool_option Proof.show_main_goal)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
304 |
("global-timing", ("Whether to enable timing in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
305 |
bool_option Library.timing)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
306 |
("theorem-dependencies", ("Whether to track theorem dependencies within Proof General.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
307 |
thm_deps_option)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
308 |
("goals-limit", ("Setting for maximum number of goals printed in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
309 |
nat_option goals_limit)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
310 |
("prems-limit", ("Setting for maximum number of premises printed in Isabelle/Isar.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
311 |
nat_option ProofContext.prems_limit)), |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
312 |
("print-depth", ("Setting for the ML print depth in Isabelle.", |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
313 |
print_depth_option))]; |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
314 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
315 |
|
14675 | 316 |
(* sending PGIP commands to the interface *) |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
317 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
318 |
fun issue_pgip pgips = notify (XML.element "pgip" [] pgips); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
319 |
|
14725 | 320 |
fun usespgml () = |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
321 |
issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []]; |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
322 |
|
14675 | 323 |
(*NB: the default returned here is actually the current value, so |
324 |
repeated uses of <askprefs> will not work correctly*) |
|
14725 | 325 |
fun show_options () = issue_pgip (map |
14568 | 326 |
(fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref" |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
327 |
[("type", ty), ("descr", descr), ("default", get ())] [name])) (!options)); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
328 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
329 |
fun set_option name value = (case assoc (!options, name) of |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
330 |
None => warning ("Unknown option: " ^ quote name) |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
331 |
| Some (_, (_, _, set)) => set value); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
332 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
333 |
fun get_option name = (case assoc (!options, name) of |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
334 |
None => warning ("Unknown option: " ^ quote name) |
14725 | 335 |
| Some (_, (_, get, _)) => |
336 |
issue_pgip [XML.element "prefval" [("name", name)] [get ()]]); |
|
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
337 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
338 |
|
14675 | 339 |
(* processing PGIP commands from the interface *) |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
340 |
|
14675 | 341 |
(*FIXME: matching on attributes is a bit too strict here*) |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
342 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
343 |
fun process_pgip_element pgip = (case pgip of |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
344 |
XML.Elem ("askpgml", _, []) => usespgml () |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
345 |
| XML.Elem ("askprefs", _, []) => show_options () |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
346 |
| XML.Elem ("getpref", [("name", name)], []) => get_option name |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
347 |
| XML.Elem ("setpref", [("name", name)], [XML.Text value]) => |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
348 |
set_option name value |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
349 |
| XML.Elem (e, _, _) => warning ("Unrecognized PGIP command: " ^ e) |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
350 |
| XML.Text t => warning ("Unrecognized PGIP command:\n" ^ t)); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
351 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
352 |
fun process_pgip s = (case XML.tree_of_string s of |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
353 |
XML.Elem ("pgip", _, pgips) => seq process_pgip_element pgips |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
354 |
| _ => warning ("Invalid PGIP packet received\n" ^ s)); |
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
355 |
|
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
356 |
|
12778 | 357 |
(* misc commands for ProofGeneral/isa *) |
358 |
||
359 |
fun thms_containing ss = |
|
13284 | 360 |
ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss; |
12778 | 361 |
|
362 |
val welcome = priority o Session.welcome; |
|
363 |
val help = welcome; |
|
364 |
val show_context = Context.the_context; |
|
365 |
||
366 |
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ()); |
|
367 |
||
368 |
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f; |
|
369 |
||
370 |
fun repeat_undo 0 = () |
|
371 |
| repeat_undo 1 = undo () |
|
372 |
| repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1)); |
|
373 |
||
374 |
||
375 |
(* restart top-level loop (keeps most state information) *) |
|
376 |
||
377 |
local |
|
378 |
||
379 |
fun restart isar = |
|
380 |
(if isar then tell_clear_goals () else kill_goal (); |
|
381 |
tell_clear_response (); |
|
382 |
welcome ()); |
|
383 |
||
384 |
in |
|
385 |
||
386 |
fun isa_restart () = restart false; |
|
387 |
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART); |
|
388 |
||
389 |
end; |
|
390 |
||
391 |
||
12833 | 392 |
fun full_proofs true = proofs := 2 |
393 |
| full_proofs false = proofs := 1; |
|
394 |
||
395 |
||
12778 | 396 |
(* outer syntax *) |
397 |
||
398 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
|
399 |
||
400 |
val undoP = |
|
401 |
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control |
|
402 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); |
|
403 |
||
404 |
val context_thy_onlyP = |
|
405 |
OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
|
406 |
(P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); |
|
407 |
||
408 |
val try_context_thy_onlyP = |
|
409 |
OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control |
|
410 |
(P.name >> (Toplevel.no_timing oo |
|
411 |
(Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); |
|
412 |
||
413 |
val restartP = |
|
414 |
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control |
|
415 |
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart))); |
|
416 |
||
417 |
val kill_proofP = |
|
418 |
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control |
|
419 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); |
|
420 |
||
421 |
val inform_file_processedP = |
|
422 |
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control |
|
423 |
(P.name >> (Toplevel.no_timing oo |
|
424 |
(fn name => Toplevel.keep (proper_inform_file_processed name)))); |
|
425 |
||
426 |
val inform_file_retractedP = |
|
427 |
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
|
428 |
(P.name >> (Toplevel.no_timing oo |
|
429 |
(fn name => Toplevel.imperative (fn () => inform_file_retracted name)))); |
|
430 |
||
14725 | 431 |
val process_pgipP = |
432 |
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control |
|
433 |
(P.text >> (Toplevel.no_timing oo |
|
434 |
(fn txt => Toplevel.imperative (fn () => process_pgip txt)))); |
|
435 |
||
12778 | 436 |
fun init_outer_syntax () = OuterSyntax.add_parsers |
14675 | 437 |
[undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
14725 | 438 |
inform_file_processedP, inform_file_retractedP, process_pgipP]; |
12778 | 439 |
|
440 |
end; |
|
441 |
||
442 |
||
443 |
(* init *) |
|
444 |
||
445 |
val initialized = ref false; |
|
446 |
||
447 |
fun init isar = |
|
448 |
(conditional (not (! initialized)) (fn () => |
|
449 |
(if isar then setmp warning_fn (K ()) init_outer_syntax () else (); |
|
450 |
setup_xsymbols_output (); |
|
451 |
setup_messages (); |
|
452 |
setup_state (); |
|
453 |
setup_thy_loader (); |
|
13526 | 454 |
setup_present_hook (); |
12778 | 455 |
set initialized; ())); |
456 |
sync_thy_loader (); |
|
457 |
print_mode := proof_generalN :: (! print_mode \ proof_generalN); |
|
458 |
set quick_and_dirty; |
|
459 |
ThmDeps.enable (); |
|
460 |
if isar then ml_prompts "ML> " "ML# " |
|
461 |
else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373"); |
|
462 |
if isar then (welcome (); Isar.sync_main ()) else isa_restart ()); |
|
463 |
||
464 |
||
465 |
||
466 |
(** generate keyword classification file **) |
|
467 |
||
468 |
local |
|
469 |
||
470 |
val regexp_meta = explode ".*+?[]^$"; |
|
471 |
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode; |
|
472 |
||
473 |
fun defconst name strs = |
|
474 |
"\n(defconst isar-keywords-" ^ name ^ |
|
475 |
"\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; |
|
476 |
||
477 |
fun make_elisp_commands commands kind = |
|
478 |
defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands); |
|
479 |
||
480 |
fun make_elisp_syntax (keywords, commands) = |
|
481 |
";;\n\ |
|
482 |
\;; Keyword classification tables for Isabelle/Isar.\n\ |
|
483 |
\;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\ |
|
484 |
\;;\n\ |
|
485 |
\;; $" ^ "Id$\n\ |
|
486 |
\;;\n" ^ |
|
487 |
defconst "major" (map #1 commands) ^ |
|
14675 | 488 |
defconst "minor" (filter Syntax.is_ascii_identifier keywords) ^ |
12778 | 489 |
implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ |
490 |
"\n(provide 'isar-keywords)\n"; |
|
491 |
||
492 |
in |
|
493 |
||
494 |
fun write_keywords s = |
|
495 |
(init_outer_syntax (); |
|
496 |
File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el")) |
|
497 |
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()))); |
|
498 |
||
499 |
end; |
|
500 |
||
501 |
end; |