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 also http://proofgeneral.inf.ed.ac.uk
9 signature PROOF_GENERAL =
11 val test_markupN: string
12 val init: bool -> unit
13 val init_outer_syntax: unit -> unit
14 val sendback: string -> Pretty.T list -> unit
17 structure ProofGeneral: PROOF_GENERAL =
23 val proof_generalN = "ProofGeneralEmacs"; (*token markup (colouring vars, etc.)*)
24 val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*)
25 val thm_depsN = "thm_deps"; (*meta-information about theorem deps*)
26 val test_markupN = "test_markup"; (*XML markup for everything*)
28 val _ = Markup.add_mode test_markupN (fn (name, props) =>
29 if name = Markup.promptN then ("", "") else XML.output_markup (name, props));
32 if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167)
36 (* text output: print modes for xsymbol *)
40 fun xsym_output "\\" = "\\\\"
41 | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
43 fun xsymbols_output s =
44 if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
45 let val syms = Symbol.explode s
46 in (implode (map xsym_output syms), Symbol.length syms) end
47 else Output.default_output s;
51 fun setup_xsymbols_output () =
52 Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
59 val _ = Markup.add_mode proof_generalN (fn (name, props) =>
62 if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
63 else if name = Markup.sendbackN then (special "376", special "377")
64 else if name = Markup.hiliteN then (special "327", special "330")
65 else if name = Markup.tclassN then (special "351", special "350")
66 else if name = Markup.tfreeN then (special "352", special "350")
67 else if name = Markup.tvarN then (special "353", special "350")
68 else if name = Markup.freeN then (special "354", special "350")
69 else if name = Markup.boundN then (special "355", special "350")
70 else if name = Markup.varN then (special "356", special "350")
71 else if name = Markup.skolemN then (special "357", special "350")
74 if name <> Markup.promptN andalso print_mode_active test_markupN
75 then XML.output_markup (name, props)
77 in (bg1 ^ bg2, en2 ^ en1) end);
80 (* messages and notification *)
82 fun decorate bg en prfx =
83 Output.writeln_default o enclose bg en o prefix_lines prfx;
85 fun setup_messages () =
86 (Output.writeln_fn := Output.writeln_default;
87 Output.status_fn := (fn "" => () | s => ! Output.priority_fn s);
88 Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
89 Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
90 Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
91 Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
92 Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
93 Output.prompt_fn := (fn s => Output.std_output (s ^ special "372")));
96 (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
98 fun emacs_notify s = decorate (special "360") (special "361") "" s;
100 fun tell_clear_goals () =
101 emacs_notify "Proof General, please clear the goals buffer.";
103 fun tell_clear_response () =
104 emacs_notify "Proof General, please clear the response buffer.";
106 fun tell_file_loaded path =
107 emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
109 fun tell_file_retracted path =
110 emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
112 fun sendback heading prts =
113 Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
116 (* theory loader actions *)
120 fun trace_action action name =
121 if action = ThyInfo.Update then
122 List.app tell_file_loaded (ThyInfo.loaded_files name)
123 else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
124 List.app tell_file_retracted (ThyInfo.loaded_files name)
128 fun setup_thy_loader () = ThyInfo.add_hook trace_action;
129 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
133 (* get informed about files *)
135 (*liberal low-level version*)
136 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
138 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
140 fun inform_file_processed file =
142 val name = thy_name file;
143 val _ = name = "" andalso error ("Bad file name: " ^ quote file);
145 if ThyInfo.check_known_thy name then
146 (Isar.>> Toplevel.commit_exit; ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
148 (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
149 tell_file_retracted (ThyLoad.thy_path name))
151 val _ = Isar.init_point ();
155 (* restart top-level loop (keeps most state information) *)
157 val welcome = priority o Session.welcome;
162 tell_clear_response ();
167 (* theorem dependency output *)
171 val spaces_quote = space_implode " " o map quote;
173 fun thm_deps_message (thms, deps) =
174 emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
176 fun tell_thm_deps ths =
177 if print_mode_active thm_depsN then
179 val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
180 val deps = Symtab.keys (fold Proofterm.thms_of_proof'
181 (map Thm.proof_of ths) Symtab.empty);
183 if null names orelse null deps then ()
184 else thm_deps_message (spaces_quote names, spaces_quote deps)
190 fun setup_present_hook () =
191 ProofDisplay.add_hook (fn res => tell_thm_deps (maps #2 res));
196 (* additional outer syntax for Isar *)
198 local structure P = OuterParse and K = OuterKeyword in
200 fun undoP () = (*undo without output -- historical*)
201 OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
202 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
205 OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
206 (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
209 OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
210 (Scan.succeed (Toplevel.no_timing o
211 Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
213 fun inform_file_processedP () =
214 OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
215 (P.name >> (fn file =>
216 Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
218 fun inform_file_retractedP () =
219 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
220 (P.name >> (Toplevel.no_timing oo
221 (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
223 fun process_pgipP () =
224 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
225 (P.text >> (Toplevel.no_timing oo
226 (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
228 fun init_outer_syntax () = List.app (fn f => f ())
229 [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
236 val initialized = ref false;
238 fun init false = panic "No Proof General interface support for Isabelle/classic mode."
240 (! initialized orelse
241 (Output.no_warnings init_outer_syntax ();
242 setup_xsymbols_output ();
244 ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
246 setup_present_hook ();
249 change print_mode (update (op =) proof_generalN);
250 Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});