equal
deleted
inserted
replaced
95 fun run_action_function f = |
95 fun run_action_function f = |
96 f () handle exn => |
96 f () handle exn => |
97 if Exn.is_interrupt exn then Exn.reraise exn |
97 if Exn.is_interrupt exn then Exn.reraise exn |
98 else print_exn exn; |
98 else print_exn exn; |
99 |
99 |
100 fun make_action_string ({index, label, name, ...} : action_context) = |
100 fun make_action_path ({index, label, name, ...} : action_context) = |
101 if label = "" then string_of_int index ^ "." ^ name else label; |
101 Path.basic (if label = "" then string_of_int index ^ "." ^ name else label); |
102 |
|
103 val make_action_path = Path.basic o make_action_string; |
|
104 |
102 |
105 fun finalize_action ({finalize, ...} : action) context = |
103 fun finalize_action ({finalize, ...} : action) context = |
106 let |
104 let |
107 val s = run_action_function finalize; |
105 val s = run_action_function finalize; |
108 val action_path = make_action_path context; |
106 val action_path = make_action_path context; |
109 val export_name = |
107 val export_name = |
110 Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); |
108 Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); |
111 val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log") |
|
112 (prefix_lines (make_action_string context ^ " finalize ") (YXML.content_of s) ^ "\n") |
|
113 in |
109 in |
114 if s <> "" then |
110 if s <> "" then |
115 Export.export \<^theory> export_name [XML.Text s] |
111 Export.export \<^theory> export_name [XML.Text s] |
116 else |
112 else |
117 () |
113 () |
126 val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); |
122 val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); |
127 val export_name = |
123 val export_name = |
128 Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + |
124 Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + |
129 line_path + offset_path); |
125 line_path + offset_path); |
130 val s = run_action_function (fn () => run_action command); |
126 val s = run_action_function (fn () => run_action command); |
131 val prefix = make_action_string context ^ " goal." ^ StringCvt.padRight #" " 6 (#name command) ^ |
|
132 Context.theory_long_name thy ^ " " ^ |
|
133 string_of_int (the (Position.line_of pos)) ^ ":" ^ |
|
134 string_of_int (the (Position.offset_of pos)) ^ " " |
|
135 val _ = Substring.triml |
|
136 val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log") |
|
137 (prefix_lines prefix (YXML.content_of s) ^ "\n") |
|
138 in |
127 in |
139 if s <> "" then |
128 if s <> "" then |
140 Export.export thy export_name [XML.Text s] |
129 Export.export thy export_name [XML.Text s] |
141 else |
130 else |
142 () |
131 () |
201 let |
190 let |
202 val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>; |
191 val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>; |
203 val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>; |
192 val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>; |
204 val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>; |
193 val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>; |
205 val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>; |
194 val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>; |
206 val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close> |
195 val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>; |
207 |> Path.explode |
|
208 |> Isabelle_System.make_directory; |
|
209 val check_theory = check_theories (space_explode "," mirabelle_theories); |
196 val check_theory = check_theories (space_explode "," mirabelle_theories); |
210 |
197 |
211 fun make_commands (thy_index, (thy, segments)) = |
198 fun make_commands (thy_index, (thy, segments)) = |
212 let |
199 let |
213 val thy_long_name = Context.theory_long_name thy; |
200 val thy_long_name = Context.theory_long_name thy; |
237 val make_action = |
224 val make_action = |
238 (case get_action name of |
225 (case get_action name of |
239 SOME f => f |
226 SOME f => f |
240 | NONE => error "Unknown action"); |
227 | NONE => error "Unknown action"); |
241 val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label; |
228 val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label; |
242 val output_dir = Path.append mirabelle_output_dir (Path.basic action_subdir); |
229 val output_dir = |
|
230 Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir); |
243 val context = |
231 val context = |
244 {index = n, label = label, name = name, arguments = args, |
232 {index = n, label = label, name = name, arguments = args, |
245 timeout = mirabelle_timeout, output_dir = output_dir}; |
233 timeout = mirabelle_timeout, output_dir = output_dir}; |
246 in |
234 in |
247 (make_action context, context) |
235 (make_action context, context) |