aspinall@21642
|
1 |
(* Title: Pure/ProofGeneral/proof_general_emacs.ML
|
aspinall@21642
|
2 |
Author: David Aspinall and Markus Wenzel
|
aspinall@21642
|
3 |
|
aspinall@21642
|
4 |
Isabelle/Isar configuration for Emacs Proof General.
|
wenzelm@26549
|
5 |
See also http://proofgeneral.inf.ed.ac.uk
|
aspinall@21642
|
6 |
*)
|
aspinall@21642
|
7 |
|
aspinall@21642
|
8 |
signature PROOF_GENERAL =
|
aspinall@21642
|
9 |
sig
|
wenzelm@26549
|
10 |
val test_markupN: string
|
aspinall@21642
|
11 |
val init: bool -> unit
|
wenzelm@24874
|
12 |
val init_outer_syntax: unit -> unit
|
wenzelm@24289
|
13 |
val sendback: string -> Pretty.T list -> unit
|
aspinall@21642
|
14 |
end;
|
aspinall@21642
|
15 |
|
aspinall@21642
|
16 |
structure ProofGeneral: PROOF_GENERAL =
|
aspinall@21642
|
17 |
struct
|
aspinall@21642
|
18 |
|
wenzelm@21945
|
19 |
|
aspinall@21642
|
20 |
(* print modes *)
|
aspinall@21642
|
21 |
|
aspinall@21642
|
22 |
val proof_generalN = "ProofGeneralEmacs"; (*token markup (colouring vars, etc.)*)
|
aspinall@21642
|
23 |
val thm_depsN = "thm_deps"; (*meta-information about theorem deps*)
|
wenzelm@26549
|
24 |
val test_markupN = "test_markup"; (*XML markup for everything*)
|
wenzelm@26549
|
25 |
|
wenzelm@29322
|
26 |
fun special ch = Symbol.SOH ^ ch;
|
aspinall@21642
|
27 |
|
aspinall@21642
|
28 |
|
wenzelm@29327
|
29 |
(* render markup *)
|
aspinall@21642
|
30 |
|
aspinall@21642
|
31 |
local
|
aspinall@21642
|
32 |
|
wenzelm@29327
|
33 |
fun render_trees ts = fold render_tree ts
|
wenzelm@29327
|
34 |
and render_tree (XML.Text s) = Buffer.add s
|
wenzelm@29327
|
35 |
| render_tree (XML.Elem (name, props, ts)) =
|
wenzelm@29327
|
36 |
let
|
wenzelm@29327
|
37 |
val (bg1, en1) =
|
wenzelm@29327
|
38 |
if name <> Markup.promptN andalso print_mode_active test_markupN
|
wenzelm@29327
|
39 |
then XML.output_markup (name, props)
|
wenzelm@29327
|
40 |
else Markup.no_output;
|
wenzelm@29327
|
41 |
val (bg2, en2) =
|
wenzelm@30292
|
42 |
if null ts then Markup.no_output
|
wenzelm@29327
|
43 |
else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
|
wenzelm@29327
|
44 |
else if name = Markup.sendbackN then (special "W", special "X")
|
wenzelm@29327
|
45 |
else if name = Markup.hiliteN then (special "0", special "1")
|
wenzelm@29327
|
46 |
else if name = Markup.tclassN then (special "B", special "A")
|
wenzelm@29327
|
47 |
else if name = Markup.tfreeN then (special "C", special "A")
|
wenzelm@29327
|
48 |
else if name = Markup.tvarN then (special "D", special "A")
|
wenzelm@29327
|
49 |
else if name = Markup.freeN then (special "E", special "A")
|
wenzelm@29327
|
50 |
else if name = Markup.boundN then (special "F", special "A")
|
wenzelm@29327
|
51 |
else if name = Markup.varN then (special "G", special "A")
|
wenzelm@29327
|
52 |
else if name = Markup.skolemN then (special "H", special "A")
|
wenzelm@29327
|
53 |
else Markup.no_output;
|
wenzelm@29327
|
54 |
in
|
wenzelm@29327
|
55 |
Buffer.add bg1 #>
|
wenzelm@29327
|
56 |
Buffer.add bg2 #>
|
wenzelm@29327
|
57 |
render_trees ts #>
|
wenzelm@29327
|
58 |
Buffer.add en2 #>
|
wenzelm@29327
|
59 |
Buffer.add en1
|
wenzelm@29327
|
60 |
end;
|
aspinall@21642
|
61 |
|
aspinall@21642
|
62 |
in
|
aspinall@21642
|
63 |
|
wenzelm@29327
|
64 |
fun render text =
|
wenzelm@29327
|
65 |
Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
|
aspinall@21642
|
66 |
|
aspinall@21642
|
67 |
end;
|
aspinall@21642
|
68 |
|
aspinall@21642
|
69 |
|
wenzelm@29327
|
70 |
(* messages *)
|
wenzelm@23641
|
71 |
|
wenzelm@29327
|
72 |
fun message bg en prfx text =
|
wenzelm@29327
|
73 |
(case render text of
|
wenzelm@29327
|
74 |
"" => ()
|
wenzelm@29327
|
75 |
| s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
|
aspinall@21642
|
76 |
|
aspinall@21642
|
77 |
fun setup_messages () =
|
wenzelm@29327
|
78 |
(Output.writeln_fn := message "" "" "";
|
wenzelm@30685
|
79 |
Output.status_fn := (fn _ => ());
|
wenzelm@29327
|
80 |
Output.priority_fn := message (special "I") (special "J") "";
|
wenzelm@29327
|
81 |
Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
|
wenzelm@29327
|
82 |
Output.debug_fn := message (special "K") (special "L") "+++ ";
|
wenzelm@29327
|
83 |
Output.warning_fn := message (special "K") (special "L") "### ";
|
wenzelm@29327
|
84 |
Output.error_fn := message (special "M") (special "N") "*** ";
|
wenzelm@29327
|
85 |
Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
|
aspinall@21642
|
86 |
|
wenzelm@22699
|
87 |
fun panic s =
|
wenzelm@29327
|
88 |
(message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
|
aspinall@21642
|
89 |
|
wenzelm@29327
|
90 |
|
wenzelm@29327
|
91 |
(* notification *)
|
wenzelm@29327
|
92 |
|
wenzelm@29327
|
93 |
val emacs_notify = message (special "I") (special "J") "";
|
aspinall@21642
|
94 |
|
aspinall@21642
|
95 |
fun tell_clear_goals () =
|
wenzelm@21940
|
96 |
emacs_notify "Proof General, please clear the goals buffer.";
|
aspinall@21642
|
97 |
|
aspinall@21642
|
98 |
fun tell_clear_response () =
|
wenzelm@21940
|
99 |
emacs_notify "Proof General, please clear the response buffer.";
|
aspinall@21642
|
100 |
|
aspinall@21642
|
101 |
fun tell_file_loaded path =
|
wenzelm@21940
|
102 |
emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
|
aspinall@21642
|
103 |
|
aspinall@21642
|
104 |
fun tell_file_retracted path =
|
wenzelm@21940
|
105 |
emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
|
aspinall@21642
|
106 |
|
wenzelm@24289
|
107 |
fun sendback heading prts =
|
wenzelm@24289
|
108 |
Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
|
wenzelm@24289
|
109 |
|
aspinall@21642
|
110 |
|
aspinall@21642
|
111 |
(* theory loader actions *)
|
aspinall@21642
|
112 |
|
aspinall@21642
|
113 |
local
|
aspinall@21642
|
114 |
|
aspinall@21642
|
115 |
fun trace_action action name =
|
aspinall@21642
|
116 |
if action = ThyInfo.Update then
|
aspinall@21642
|
117 |
List.app tell_file_loaded (ThyInfo.loaded_files name)
|
aspinall@21642
|
118 |
else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
|
aspinall@21642
|
119 |
List.app tell_file_retracted (ThyInfo.loaded_files name)
|
aspinall@21642
|
120 |
else ();
|
aspinall@21642
|
121 |
|
aspinall@21642
|
122 |
in
|
aspinall@21642
|
123 |
fun setup_thy_loader () = ThyInfo.add_hook trace_action;
|
wenzelm@26613
|
124 |
fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
|
aspinall@21642
|
125 |
end;
|
aspinall@21642
|
126 |
|
aspinall@21642
|
127 |
|
wenzelm@21948
|
128 |
(* get informed about files *)
|
aspinall@21642
|
129 |
|
wenzelm@25442
|
130 |
(*liberal low-level version*)
|
wenzelm@25436
|
131 |
val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
|
aspinall@21642
|
132 |
|
aspinall@21642
|
133 |
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
|
aspinall@21642
|
134 |
|
wenzelm@27577
|
135 |
fun inform_file_processed file =
|
wenzelm@27577
|
136 |
let
|
wenzelm@27577
|
137 |
val name = thy_name file;
|
wenzelm@27577
|
138 |
val _ = name = "" andalso error ("Bad file name: " ^ quote file);
|
wenzelm@27577
|
139 |
val _ =
|
wenzelm@27577
|
140 |
if ThyInfo.check_known_thy name then
|
wenzelm@28426
|
141 |
(Isar.>> (Toplevel.commit_exit Position.none);
|
wenzelm@28426
|
142 |
ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
|
wenzelm@27585
|
143 |
handle ERROR msg =>
|
wenzelm@27591
|
144 |
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
|
wenzelm@27585
|
145 |
tell_file_retracted (ThyLoad.thy_path name))
|
wenzelm@27577
|
146 |
else ();
|
wenzelm@29349
|
147 |
val _ = Isar.init ();
|
wenzelm@27577
|
148 |
in () end;
|
aspinall@21642
|
149 |
|
aspinall@21642
|
150 |
|
aspinall@21642
|
151 |
(* restart top-level loop (keeps most state information) *)
|
aspinall@21642
|
152 |
|
aspinall@21642
|
153 |
val welcome = priority o Session.welcome;
|
aspinall@21642
|
154 |
|
aspinall@21642
|
155 |
fun restart () =
|
wenzelm@21940
|
156 |
(sync_thy_loader ();
|
wenzelm@21940
|
157 |
tell_clear_goals ();
|
wenzelm@21940
|
158 |
tell_clear_response ();
|
wenzelm@29349
|
159 |
Isar.init ();
|
wenzelm@27577
|
160 |
welcome ());
|
aspinall@21642
|
161 |
|
aspinall@21642
|
162 |
|
aspinall@21642
|
163 |
(* theorem dependency output *)
|
aspinall@21642
|
164 |
|
aspinall@21642
|
165 |
local
|
aspinall@21642
|
166 |
|
aspinall@21642
|
167 |
val spaces_quote = space_implode " " o map quote;
|
aspinall@21642
|
168 |
|
aspinall@21642
|
169 |
fun thm_deps_message (thms, deps) =
|
wenzelm@21948
|
170 |
emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
|
aspinall@21642
|
171 |
|
wenzelm@28096
|
172 |
in
|
wenzelm@28096
|
173 |
|
wenzelm@28103
|
174 |
fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
|
wenzelm@28106
|
175 |
if print_mode_active thm_depsN andalso
|
wenzelm@28106
|
176 |
can Toplevel.theory_of state andalso Toplevel.is_theory state'
|
wenzelm@28106
|
177 |
then
|
wenzelm@28100
|
178 |
let val (names, deps) =
|
wenzelm@28100
|
179 |
ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
|
wenzelm@28100
|
180 |
in
|
wenzelm@21968
|
181 |
if null names orelse null deps then ()
|
wenzelm@21968
|
182 |
else thm_deps_message (spaces_quote names, spaces_quote deps)
|
wenzelm@21968
|
183 |
end
|
wenzelm@28096
|
184 |
else ());
|
aspinall@21642
|
185 |
|
aspinall@21642
|
186 |
end;
|
aspinall@21642
|
187 |
|
aspinall@21642
|
188 |
|
aspinall@21642
|
189 |
(* additional outer syntax for Isar *)
|
aspinall@21642
|
190 |
|
aspinall@21642
|
191 |
local structure P = OuterParse and K = OuterKeyword in
|
aspinall@21642
|
192 |
|
wenzelm@33872
|
193 |
fun prP () =
|
wenzelm@33872
|
194 |
OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
|
wenzelm@33872
|
195 |
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
|
wenzelm@33872
|
196 |
if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
|
wenzelm@33872
|
197 |
else (Toplevel.quiet := false; Toplevel.print_state true state))));
|
wenzelm@33872
|
198 |
|
wenzelm@25192
|
199 |
fun undoP () = (*undo without output -- historical*)
|
aspinall@21642
|
200 |
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
|
wenzelm@27535
|
201 |
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
|
aspinall@21642
|
202 |
|
wenzelm@24867
|
203 |
fun restartP () =
|
aspinall@21642
|
204 |
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
|
aspinall@21642
|
205 |
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
|
aspinall@21642
|
206 |
|
wenzelm@24867
|
207 |
fun kill_proofP () =
|
aspinall@21642
|
208 |
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
|
wenzelm@27532
|
209 |
(Scan.succeed (Toplevel.no_timing o
|
wenzelm@27532
|
210 |
Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
|
wenzelm@27532
|
211 |
|
wenzelm@24867
|
212 |
fun inform_file_processedP () =
|
aspinall@21642
|
213 |
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
|
wenzelm@27577
|
214 |
(P.name >> (fn file =>
|
wenzelm@27577
|
215 |
Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
|
aspinall@21642
|
216 |
|
wenzelm@24867
|
217 |
fun inform_file_retractedP () =
|
aspinall@21642
|
218 |
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
|
aspinall@21642
|
219 |
(P.name >> (Toplevel.no_timing oo
|
aspinall@21642
|
220 |
(fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
|
aspinall@21642
|
221 |
|
wenzelm@24867
|
222 |
fun process_pgipP () =
|
aspinall@21642
|
223 |
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
|
aspinall@21642
|
224 |
(P.text >> (Toplevel.no_timing oo
|
aspinall@21642
|
225 |
(fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
|
aspinall@21642
|
226 |
|
wenzelm@24867
|
227 |
fun init_outer_syntax () = List.app (fn f => f ())
|
wenzelm@33872
|
228 |
[prP, undoP, restartP, kill_proofP, inform_file_processedP,
|
wenzelm@33872
|
229 |
inform_file_retractedP, process_pgipP];
|
aspinall@21642
|
230 |
|
aspinall@21642
|
231 |
end;
|
aspinall@21642
|
232 |
|
aspinall@21642
|
233 |
|
aspinall@21642
|
234 |
(* init *)
|
aspinall@21642
|
235 |
|
wenzelm@32738
|
236 |
val initialized = Unsynchronized.ref false;
|
aspinall@21642
|
237 |
|
wenzelm@22699
|
238 |
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
|
wenzelm@21940
|
239 |
| init true =
|
wenzelm@21968
|
240 |
(! initialized orelse
|
wenzelm@32966
|
241 |
(Output.no_warnings_CRITICAL init_outer_syntax ();
|
wenzelm@29327
|
242 |
Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
|
wenzelm@29327
|
243 |
Output.add_mode proof_generalN Output.default_output Output.default_escape;
|
wenzelm@29327
|
244 |
Markup.add_mode proof_generalN YXML.output_markup;
|
wenzelm@21968
|
245 |
setup_messages ();
|
wenzelm@22590
|
246 |
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
|
wenzelm@21968
|
247 |
setup_thy_loader ();
|
wenzelm@21968
|
248 |
setup_present_hook ();
|
wenzelm@32738
|
249 |
Unsynchronized.set initialized);
|
wenzelm@21968
|
250 |
sync_thy_loader ();
|
wenzelm@32738
|
251 |
Unsynchronized.change print_mode (update (op =) proof_generalN);
|
wenzelm@26643
|
252 |
Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
|
aspinall@21642
|
253 |
|
aspinall@21642
|
254 |
end;
|