author | wenzelm |
Sat, 08 Dec 2001 16:13:20 +0100 | |
changeset 12424 | 3c70d99b7586 |
parent 12422 | 7389066a4df9 |
child 12592 | 0eb1685a00b4 |
permissions | -rw-r--r-- |
6699 | 1 |
(* Title: Pure/Interface/proof_general.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
9507 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6699 | 5 |
|
10078 | 6 |
Isabelle configuration for Proof General (see http://www.proofgeneral.org). |
6699 | 7 |
*) |
8 |
||
9 |
signature PROOF_GENERAL = |
|
10 |
sig |
|
11 |
val setup: (theory -> theory) list |
|
7954 | 12 |
val update_thy_only: string -> unit |
13 |
val try_update_thy_only: string -> unit |
|
14 |
val inform_file_processed: string -> unit |
|
15 |
val inform_file_retracted: string -> unit |
|
11017 | 16 |
val thms_containing: string list -> unit |
7193 | 17 |
val help: unit -> unit |
18 |
val show_context: unit -> theory |
|
19 |
val kill_goal: unit -> unit |
|
20 |
val repeat_undo: int -> unit |
|
7235 | 21 |
val isa_restart: unit -> unit |
6699 | 22 |
val init: bool -> unit |
12217 | 23 |
val write_keywords: string -> unit |
6699 | 24 |
end; |
25 |
||
26 |
structure ProofGeneral: PROOF_GENERAL = |
|
27 |
struct |
|
28 |
||
12422 | 29 |
(* print modes *) |
30 |
||
31 |
val proof_generalN = "ProofGeneral"; |
|
32 |
val xsymbolsN = "xsymbols"; |
|
33 |
||
34 |
val pgmlN = "PGML"; |
|
35 |
fun pgml () = pgmlN mem_string ! print_mode; |
|
36 |
||
37 |
||
38 |
(* text output *) |
|
39 |
||
40 |
local |
|
41 |
||
42 |
fun xsymbols_output s = |
|
43 |
if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then |
|
44 |
let val syms = Symbol.explode s |
|
45 |
in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end |
|
46 |
else (s, real (size s)); |
|
47 |
||
48 |
fun pgml_output (s, len) = |
|
49 |
if pgml () then (XML.text s, len) |
|
50 |
else (s, len); |
|
51 |
||
52 |
in |
|
53 |
||
54 |
fun setup_xsymbols_output () = |
|
55 |
Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent); |
|
56 |
||
57 |
end; |
|
58 |
||
6699 | 59 |
|
60 |
(* token translations *) |
|
61 |
||
62 |
local |
|
63 |
||
64 |
val end_tag = oct_char "350"; |
|
12422 | 65 |
val class_tag = ("class", oct_char "351"); |
66 |
val tfree_tag = ("tfree", oct_char "352"); |
|
67 |
val tvar_tag = ("tvar", oct_char "353"); |
|
68 |
val free_tag = ("free", oct_char "354"); |
|
69 |
val bound_tag = ("bound", oct_char "355"); |
|
70 |
val var_tag = ("var", oct_char "356"); |
|
71 |
val skolem_tag = ("skolem", oct_char "357"); |
|
6699 | 72 |
|
12422 | 73 |
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; |
74 |
||
75 |
fun tagit (kind, bg_tag) x = |
|
76 |
(if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag, |
|
77 |
real (Symbol.length (Symbol.explode x))); |
|
6699 | 78 |
|
9918 | 79 |
fun free_or_skolem x = |
7597 | 80 |
(case try Syntax.dest_skolem x of |
9918 | 81 |
None => tagit free_tag x |
7597 | 82 |
| Some x' => tagit skolem_tag x'); |
83 |
||
9918 | 84 |
fun var_or_skolem s = |
85 |
(case Syntax.read_var s of |
|
86 |
Var ((x, i), _) => |
|
87 |
(case try Syntax.dest_skolem x of |
|
88 |
None => tagit var_tag s |
|
89 |
| Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i))) |
|
90 |
| _ => tagit var_tag s); |
|
91 |
||
6699 | 92 |
val proof_general_trans = |
93 |
Syntax.tokentrans_mode proof_generalN |
|
12422 | 94 |
[("class", tagit class_tag), |
6699 | 95 |
("tfree", tagit tfree_tag), |
96 |
("tvar", tagit tvar_tag), |
|
9918 | 97 |
("free", free_or_skolem), |
6699 | 98 |
("bound", tagit bound_tag), |
9918 | 99 |
("var", var_or_skolem)]; |
6699 | 100 |
|
12422 | 101 |
in val setup = [Theory.add_tokentrfuns proof_general_trans] end; |
6699 | 102 |
|
103 |
||
104 |
||
12422 | 105 |
(* messages and notification *) |
8445 | 106 |
|
12422 | 107 |
local |
108 |
||
109 |
fun decorated_output bg en prfx = |
|
110 |
writeln_default o enclose bg en o prefix_lines prfx; |
|
8445 | 111 |
|
12422 | 112 |
fun message kind bg en prfx s = |
113 |
if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s]) |
|
114 |
else decorated_output bg en prfx s; |
|
6699 | 115 |
|
12422 | 116 |
val notify = message "notify" (oct_char "360") (oct_char "361") ""; |
7193 | 117 |
|
12422 | 118 |
in |
6699 | 119 |
|
120 |
fun setup_messages () = |
|
12422 | 121 |
(writeln_fn := message "output" "" "" ""; |
122 |
priority_fn := message "information" (oct_char "360") (oct_char "361") ""; |
|
123 |
tracing_fn := message "tracing" (oct_char "360") (oct_char "361") (oct_char "375"); |
|
124 |
warning_fn := message "warning" (oct_char "362") (oct_char "363") "### "; |
|
125 |
error_fn := message "error" (oct_char "364") (oct_char "365") "*** "); |
|
6699 | 126 |
|
12422 | 127 |
fun tell_clear_goals () = notify "Proof General, please clear the goals buffer."; |
128 |
fun tell_clear_response () = notify "Proof General, please clear the response buffer."; |
|
129 |
fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path)); |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
130 |
|
12422 | 131 |
end; |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
132 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
133 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
134 |
(* theory / proof state output *) |
6699 | 135 |
|
12422 | 136 |
local |
137 |
||
138 |
fun tmp_markers f = |
|
139 |
setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f (); |
|
140 |
||
141 |
fun statedisplay prts = |
|
142 |
writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]); |
|
143 |
||
144 |
fun print_current_goals n m st = |
|
145 |
if pgml () then statedisplay (Display.pretty_current_goals n m st) |
|
146 |
else tmp_markers (fn () => Display.print_current_goals_default n m st); |
|
147 |
||
148 |
fun print_state b st = |
|
149 |
if pgml () then statedisplay (Toplevel.pretty_state b st) |
|
150 |
else tmp_markers (fn () => Toplevel.print_state_default b st); |
|
151 |
||
152 |
in |
|
153 |
||
7939 | 154 |
fun setup_state () = |
12422 | 155 |
(Display.print_current_goals_fn := print_current_goals; |
156 |
Toplevel.print_state_fn := print_state; |
|
9761
21a11b9da318
improved handling of messages: do not decorate writeln output;
wenzelm
parents:
9697
diff
changeset
|
157 |
Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default)); |
6699 | 158 |
|
12422 | 159 |
end; |
160 |
||
6699 | 161 |
|
7100 | 162 |
(* theory loader actions *) |
163 |
||
164 |
local |
|
165 |
||
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
166 |
fun add_master_files name files = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
167 |
let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name] |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
168 |
in masters @ gen_rems (op = o pairself Path.base) (files, masters) end; |
7100 | 169 |
|
7893 | 170 |
fun trace_action action name = |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
171 |
if action = ThyInfo.Update then |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
172 |
seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name) |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
173 |
else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
174 |
seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name)) |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
175 |
else (); |
7193 | 176 |
|
7100 | 177 |
in |
7893 | 178 |
fun setup_thy_loader () = ThyInfo.add_hook trace_action; |
7100 | 179 |
end; |
180 |
||
181 |
||
7954 | 182 |
(* prepare theory context *) |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
183 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
184 |
val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack; |
10417
42e6b8502d52
Moved rewriting functions from Thm to MetaSimplifier.
berghofe
parents:
10246
diff
changeset
|
185 |
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only; |
7954 | 186 |
|
187 |
fun which_context () = |
|
188 |
(case Context.get_context () of |
|
189 |
Some thy => " Using current (dynamic!) one: " ^ |
|
7956 | 190 |
(case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>") |
7954 | 191 |
| None => ""); |
192 |
||
193 |
fun try_update_thy_only file = |
|
9662 | 194 |
ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () => |
7954 | 195 |
let val name = thy_name file in |
196 |
if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name |
|
197 |
else warning ("Unkown theory context of ML file." ^ which_context ()) |
|
198 |
end) (); |
|
199 |
||
200 |
||
201 |
(* get informed about files *) |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
202 |
|
9821
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
203 |
val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys; |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
204 |
|
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
205 |
val inform_file_processed = touch_child_thys o thy_name; |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
206 |
val inform_file_retracted = touch_child_thys o thy_name; |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
207 |
|
9821
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
208 |
fun proper_inform_file_processed file state = |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
209 |
let val name = thy_name file in |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
210 |
touch_child_thys name; |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
211 |
if not (Toplevel.is_toplevel state) then |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
212 |
warning ("Not at toplevel -- cannot register theory " ^ quote name) |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
213 |
else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg => |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
214 |
(warning msg; warning ("Failed to register theory " ^ quote name)) |
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
215 |
end; |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
216 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
217 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
218 |
(* misc commands for ProofGeneral/isa *) |
7193 | 219 |
|
11017 | 220 |
fun thms_containing ss = |
221 |
let |
|
222 |
val thy = the_context (); |
|
223 |
fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT)); |
|
224 |
in ThmDatabase.print_thms_containing thy (map read_term ss) end; |
|
7579 | 225 |
|
9775 | 226 |
val welcome = priority o Session.welcome; |
9761
21a11b9da318
improved handling of messages: do not decorate writeln output;
wenzelm
parents:
9697
diff
changeset
|
227 |
val help = welcome; |
7193 | 228 |
val show_context = Context.the_context; |
229 |
||
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
230 |
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ()); |
7193 | 231 |
|
11888 | 232 |
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f; |
7922 | 233 |
|
7193 | 234 |
fun repeat_undo 0 = () |
7922 | 235 |
| repeat_undo 1 = undo () |
236 |
| repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1)); |
|
7193 | 237 |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
238 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
239 |
(* re-init process (an approximation) *) |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
240 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
241 |
local |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
242 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
243 |
fun restart isar = |
9497 | 244 |
(if isar then tell_clear_goals () else kill_goal (); |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
245 |
tell_clear_response (); |
9761
21a11b9da318
improved handling of messages: do not decorate writeln output;
wenzelm
parents:
9697
diff
changeset
|
246 |
welcome ()); |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
247 |
|
12424 | 248 |
fun restart_loader () = ThyInfo.touch_all_thys (); |
9697 | 249 |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
250 |
in |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
251 |
|
9497 | 252 |
fun isa_start () = restart false; |
9697 | 253 |
fun isa_restart () = (restart_loader (); restart false); |
254 |
fun isar_restart () = (restart_loader (); restart true; raise Toplevel.RESTART); |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
255 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
256 |
end; |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
257 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
258 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
259 |
(* outer syntax *) |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
260 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
261 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
262 |
|
9821
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
263 |
val old_undoP = (*same name for compatibility with PG/Isabelle99*) |
8452 | 264 |
OuterSyntax.improper_command "undo" "undo last command (no output)" K.control |
9010 | 265 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); |
8452 | 266 |
|
8647 | 267 |
val undoP = |
9514 | 268 |
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control |
9010 | 269 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); |
8647 | 270 |
|
7954 | 271 |
val context_thy_onlyP = |
272 |
OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
|
9010 | 273 |
(P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); |
7954 | 274 |
|
275 |
val try_context_thy_onlyP = |
|
276 |
OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control |
|
9010 | 277 |
(P.name >> (Toplevel.no_timing oo |
278 |
(Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); |
|
7954 | 279 |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
280 |
val restartP = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
281 |
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control |
9010 | 282 |
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart))); |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
283 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
284 |
val kill_proofP = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
285 |
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control |
9010 | 286 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
287 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
288 |
val inform_file_processedP = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
289 |
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control |
9010 | 290 |
(P.name >> (Toplevel.no_timing oo |
9821
095beeef58ae
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
wenzelm
parents:
9775
diff
changeset
|
291 |
(fn name => Toplevel.keep (proper_inform_file_processed name)))); |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
292 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
293 |
val inform_file_retractedP = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
294 |
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
9010 | 295 |
(P.name >> (Toplevel.no_timing oo |
296 |
(fn name => Toplevel.imperative (fn () => inform_file_retracted name)))); |
|
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
297 |
|
7954 | 298 |
fun init_outer_syntax () = OuterSyntax.add_parsers |
8647 | 299 |
[old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
7954 | 300 |
inform_file_processedP, inform_file_retractedP]; |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
301 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
302 |
end; |
7193 | 303 |
|
304 |
||
6699 | 305 |
(* init *) |
306 |
||
307 |
fun init isar = |
|
8668 | 308 |
(if isar then setmp warning_fn (K ()) init_outer_syntax () else (); |
8452 | 309 |
setup_xsymbols_output (); |
8445 | 310 |
setup_messages (); |
7939 | 311 |
setup_state (); |
7893 | 312 |
setup_thy_loader (); |
9979 | 313 |
print_mode := proof_generalN :: ! print_mode; |
6699 | 314 |
set quick_and_dirty; |
9462 | 315 |
ThmDeps.enable (); |
316 |
if isar then ml_prompts "ML> " "ML# " |
|
317 |
else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373"); |
|
9979 | 318 |
if isar then (welcome (); Isar.sync_main ()) else isa_start ()); |
6699 | 319 |
|
320 |
||
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
321 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
322 |
(** generate keyword classification file **) |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
323 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
324 |
local |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
325 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
326 |
val regexp_meta = explode ".*+?[]^$"; |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
327 |
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode; |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
328 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
329 |
fun defconst name strs = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
330 |
"\n(defconst isar-keywords-" ^ name ^ |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
331 |
"\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
332 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
333 |
fun make_elisp_commands commands kind = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
334 |
defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands); |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
335 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
336 |
fun make_elisp_syntax (keywords, commands) = |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
337 |
";;\n\ |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
338 |
\;; Keyword classification tables for Isabelle/Isar.\n\ |
11510 | 339 |
\;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\ |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
340 |
\;;\n\ |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
341 |
\;; $" ^ "Id$\n\ |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
342 |
\;;\n" ^ |
8990 | 343 |
defconst "major" (map #1 commands) ^ |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
344 |
defconst "minor" (filter Syntax.is_identifier keywords) ^ |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
345 |
implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
346 |
"\n(provide 'isar-keywords)\n"; |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
347 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
348 |
in |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
349 |
|
12217 | 350 |
fun write_keywords s = |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
351 |
(init_outer_syntax (); |
12217 | 352 |
File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el")) |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
353 |
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()))); |
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
354 |
|
6699 | 355 |
end; |
7937
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
356 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
357 |
|
82025fe607d3
added inform_file_processed, inform_file_retracted;
wenzelm
parents:
7922
diff
changeset
|
358 |
end; |
10933 | 359 |
|
10954 | 360 |
(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*) |
10933 | 361 |
infix \\\\ val op \\\\ = op \\; |