1 (* Title: Pure/ProofGeneral/proof_general_emacs.ML
3 Author: David Aspinall and Markus Wenzel
5 Isabelle/Isar configuration for Emacs Proof General.
6 See http://proofgeneral.inf.ed.ac.uk
9 signature PROOF_GENERAL =
11 val init: bool -> unit
12 val sendback: string -> Pretty.T list -> unit
13 val write_keywords: string -> unit
16 structure ProofGeneral: PROOF_GENERAL =
22 val proof_generalN = "ProofGeneralEmacs"; (*token markup (colouring vars, etc.)*)
23 val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*)
24 val thm_depsN = "thm_deps"; (*meta-information about theorem deps*)
27 if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
31 (* text output: print modes for xsymbol *)
35 fun xsym_output "\\" = "\\\\"
36 | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
38 fun xsymbols_output s =
39 if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
40 let val syms = Symbol.explode s
41 in (implode (map xsym_output syms), Symbol.length syms) end
42 else Output.default_output s;
46 fun setup_xsymbols_output () =
47 Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
52 (* token translations *)
56 fun end_tag () = special "350";
57 val class_tag = ("class", fn () => special "351");
58 val tfree_tag = ("tfree", fn () => special "352");
59 val tvar_tag = ("tvar", fn () => special "353");
60 val free_tag = ("free", fn () => special "354");
61 val bound_tag = ("bound", fn () => special "355");
62 val var_tag = ("var", fn () => special "356");
63 val skolem_tag = ("skolem", fn () => special "357");
65 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
67 fun tagit (kind, bg_tag) x =
68 (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
70 fun free_or_skolem x =
71 (case try Name.dest_skolem x of
72 NONE => tagit free_tag x
73 | SOME x' => tagit skolem_tag x');
76 (case Lexicon.read_variable s of
78 (case try Name.dest_skolem x of
79 NONE => tagit var_tag s
80 | SOME x' => tagit skolem_tag
81 (setmp show_question_marks true Term.string_of_vname (x', i)))
82 | NONE => tagit var_tag s);
84 val proof_general_trans =
85 Syntax.tokentrans_mode proof_generalN
86 [("class", tagit class_tag),
87 ("tfree", tagit tfree_tag),
88 ("tvar", tagit tvar_tag),
89 ("free", free_or_skolem),
90 ("bound", tagit bound_tag),
91 ("var", var_or_skolem)];
95 val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
102 fun proof_general_markup (name, props) =
103 (if name = Markup.promptN then ("", special "372")
104 else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
105 else if name = Markup.sendbackN then (special "376", special "377")
106 else if name = Markup.hiliteN then (special "327", special "330")
108 |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
110 (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
111 enclose "</" ">" name ^ en));
113 val _ = Markup.add_mode proof_generalN proof_general_markup;
116 (* messages and notification *)
118 fun decorate bg en prfx =
119 Output.writeln_default o enclose bg en o prefix_lines prfx;
121 fun setup_messages () =
122 (Output.writeln_fn := Output.writeln_default;
123 Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
124 Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
125 Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
126 Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
127 Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s));
130 (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
132 fun emacs_notify s = decorate (special "360") (special "361") "" s;
134 fun tell_clear_goals () =
135 emacs_notify "Proof General, please clear the goals buffer.";
137 fun tell_clear_response () =
138 emacs_notify "Proof General, please clear the response buffer.";
140 fun tell_file_loaded path =
141 emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
143 fun tell_file_retracted path =
144 emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
146 fun sendback heading prts =
147 Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
150 (* theory loader actions *)
154 fun trace_action action name =
155 if action = ThyInfo.Update then
156 List.app tell_file_loaded (ThyInfo.loaded_files name)
157 else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
158 List.app tell_file_retracted (ThyInfo.loaded_files name)
162 fun setup_thy_loader () = ThyInfo.add_hook trace_action;
163 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
167 (* get informed about files *)
169 val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
171 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
172 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
174 fun proper_inform_file_processed file () =
175 let val name = thy_name file in
176 if ThyInfo.known_thy name then
177 (ThyInfo.touch_child_thys name;
178 ThyInfo.register_thy name handle ERROR msg =>
179 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
180 tell_file_retracted (Path.base (Path.explode file))))
181 else raise Toplevel.UNDEF
184 fun vacuous_inform_file_processed file () =
185 (warning ("No theory " ^ quote (thy_name file));
186 tell_file_retracted (Path.base (Path.explode file)));
189 (* restart top-level loop (keeps most state information) *)
191 val welcome = priority o Session.welcome;
196 tell_clear_response ();
198 raise Toplevel.RESTART);
201 (* theorem dependency output *)
205 val spaces_quote = space_implode " " o map quote;
207 fun thm_deps_message (thms, deps) =
208 emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
210 fun tell_thm_deps ths =
211 if print_mode_active thm_depsN then
213 val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
214 val deps = Symtab.keys (fold Proofterm.thms_of_proof'
215 (map Thm.proof_of ths) Symtab.empty);
217 if null names orelse null deps then ()
218 else thm_deps_message (spaces_quote names, spaces_quote deps)
224 fun setup_present_hook () =
225 Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
230 (* additional outer syntax for Isar *)
232 local structure P = OuterParse and K = OuterKeyword in
234 fun undoP () = (*undo without output*)
235 OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
236 (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
239 OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
240 (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
243 OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
244 (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
246 fun inform_file_processedP () =
247 OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
248 (P.name >> (fn file => Toplevel.no_timing o
249 Toplevel.init_empty (vacuous_inform_file_processed file) o
251 Toplevel.init_empty (proper_inform_file_processed file)));
253 fun inform_file_retractedP () =
254 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
255 (P.name >> (Toplevel.no_timing oo
256 (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
258 fun process_pgipP () =
259 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
260 (P.text >> (Toplevel.no_timing oo
261 (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
263 fun init_outer_syntax () = List.app (fn f => f ())
264 [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
271 val initialized = ref false;
273 fun init false = panic "No Proof General interface support for Isabelle/classic mode."
275 (! initialized orelse
276 (Output.no_warnings init_outer_syntax ();
277 setup_xsymbols_output ();
279 ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
281 setup_present_hook ();
284 change print_mode (cons proof_generalN o remove (op =) proof_generalN);
289 (** generate elisp file for keyword classification **)
293 val regexp_meta = member (op =) (explode ".*+?[]^$");
294 val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c);
296 fun defconst name strs =
297 "\n(defconst isar-keywords-" ^ name ^
298 "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n";
300 fun make_elisp_commands commands kind = defconst kind
301 (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
303 fun make_elisp_syntax (keywords, commands) =
305 \;; Keyword classification tables for Isabelle/Isar.\n\
306 \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
310 defconst "major" (map #1 commands) ^
311 defconst "minor" (filter Syntax.is_identifier keywords) ^
312 implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
313 "\n(provide 'isar-keywords)\n";
317 fun write_keywords s =
318 (init_outer_syntax ();
319 File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
320 (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));