author | wenzelm |
Thu, 03 Mar 2016 15:23:02 +0100 | |
changeset 62505 | 9e2a65912111 |
parent 62498 | 5dfcc9697f29 |
child 62516 | 5732f1c31566 |
permissions | -rw-r--r-- |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/runtime.ML |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
3 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
4 |
Isar toplevel runtime support. |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
5 |
*) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
6 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
7 |
signature RUNTIME = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
8 |
sig |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
9 |
exception UNDEF |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
10 |
exception EXCURSION_FAIL of exn * string |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
11 |
exception TOPLEVEL_ERROR |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
12 |
val exn_context: Proof.context option -> exn -> exn |
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
59582
diff
changeset
|
13 |
val thread_context: exn -> exn |
51285 | 14 |
type error = ((serial * string) * string option) |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
15 |
val exn_messages_ids: exn -> error list |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
16 |
val exn_messages: exn -> (serial * string) list |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
17 |
val exn_message: exn -> string |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
18 |
val exn_error_message: exn -> unit |
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
57831
diff
changeset
|
19 |
val exn_system_message: exn -> unit |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
20 |
val exn_trace: (unit -> 'a) -> 'a |
59056
cbe9563c03d1
even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents:
59055
diff
changeset
|
21 |
val exn_trace_system: (unit -> 'a) -> 'a |
62498 | 22 |
val exn_debugger: (unit -> 'a) -> 'a |
23 |
val exn_debugger_system: (unit -> 'a) -> 'a |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
24 |
val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
25 |
val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
32091
diff
changeset
|
26 |
val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
27 |
val toplevel_program: (unit -> 'a) -> 'a |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
28 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
29 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
30 |
structure Runtime: RUNTIME = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
31 |
struct |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
32 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
33 |
(** exceptions **) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
34 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
35 |
exception UNDEF; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
36 |
exception EXCURSION_FAIL of exn * string; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
37 |
exception TOPLEVEL_ERROR; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
38 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
39 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
40 |
(* exn_context *) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
41 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
42 |
exception CONTEXT of Proof.context * exn; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
43 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
44 |
fun exn_context NONE exn = exn |
39285 | 45 |
| exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn); |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
46 |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
59582
diff
changeset
|
47 |
fun thread_context exn = |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
59582
diff
changeset
|
48 |
exn_context (Option.map Context.proof_of (Context.thread_data ())) exn; |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
59582
diff
changeset
|
49 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
50 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
51 |
(* exn_message *) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
52 |
|
51285 | 53 |
type error = ((serial * string) * string option); |
54 |
||
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
55 |
local |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
56 |
|
52686 | 57 |
fun robust f x = |
58 |
(case try f x of |
|
59 |
SOME s => s |
|
60 |
| NONE => Markup.markup Markup.intensify "<malformed>"); |
|
61 |
||
62 |
fun robust2 f x y = robust (fn () => f x y) (); |
|
63 |
||
64 |
fun robust_context NONE _ _ = [] |
|
65 |
| robust_context (SOME ctxt) f xs = map (robust2 f ctxt) xs; |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
66 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
67 |
fun identify exn = |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
68 |
let |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
69 |
val exn' = Par_Exn.identify [] exn; |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
70 |
val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN; |
51242
a8e664e4fb5f
identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;
wenzelm
parents:
50914
diff
changeset
|
71 |
val i = Par_Exn.the_serial exn' handle Option.Option => serial (); |
a8e664e4fb5f
identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;
wenzelm
parents:
50914
diff
changeset
|
72 |
in ((i, exn'), exec_id) end; |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50505
diff
changeset
|
73 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
74 |
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
75 |
| flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
76 |
| flatten context exn = |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
77 |
(case Par_Exn.dest exn of |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
78 |
SOME exns => maps (flatten context) exns |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
79 |
| NONE => [(context, identify exn)]); |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50505
diff
changeset
|
80 |
|
61878 | 81 |
val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy; |
82 |
||
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
83 |
in |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
84 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
85 |
fun exn_messages_ids e = |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
86 |
let |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
87 |
fun raised exn name msgs = |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
88 |
let val pos = Position.here (Exn_Output.position exn) in |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
89 |
(case msgs of |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
90 |
[] => "exception " ^ name ^ " raised" ^ pos |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
91 |
| [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg |
51653 | 92 |
| _ => |
93 |
cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: |
|
94 |
map (Markup.markup Markup.item) msgs)) |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
95 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
96 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
97 |
fun exn_msgs (context, ((i, exn), id)) = |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
98 |
(case exn of |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
99 |
EXCURSION_FAIL (exn, loc) => |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
100 |
map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id)) |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
101 |
(sorted_msgs context exn) |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
102 |
| _ => |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
103 |
let |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
104 |
val msg = |
44247 | 105 |
(case exn of |
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
58894
diff
changeset
|
106 |
TimeLimit.TimeOut => "Timeout" |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
107 |
| TOPLEVEL_ERROR => "Error" |
57831
885888a880fb
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
wenzelm
parents:
57666
diff
changeset
|
108 |
| ERROR "" => "Error" |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
109 |
| ERROR msg => msg |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
110 |
| Fail msg => raised exn "Fail" [msg] |
61878 | 111 |
| THEORY (msg, thys) => raised exn "THEORY" (msg :: map (robust print_thy) thys) |
44247 | 112 |
| Ast.AST (msg, asts) => |
52686 | 113 |
raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts) |
44247 | 114 |
| TYPE (msg, Ts, ts) => |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
115 |
raised exn "TYPE" (msg :: |
52686 | 116 |
(robust_context context Syntax.string_of_typ Ts @ |
117 |
robust_context context Syntax.string_of_term ts)) |
|
44247 | 118 |
| TERM (msg, ts) => |
52686 | 119 |
raised exn "TERM" (msg :: robust_context context Syntax.string_of_term ts) |
51640
d022e8bd2375
improved printing of exception CTERM (see also d0f0f37ec346);
wenzelm
parents:
51639
diff
changeset
|
120 |
| CTERM (msg, cts) => |
d022e8bd2375
improved printing of exception CTERM (see also d0f0f37ec346);
wenzelm
parents:
51639
diff
changeset
|
121 |
raised exn "CTERM" |
59582 | 122 |
(msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts)) |
44247 | 123 |
| THM (msg, i, thms) => |
45487
ae60518ac054
simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents:
45486
diff
changeset
|
124 |
raised exn ("THM " ^ string_of_int i) |
61268 | 125 |
(msg :: robust_context context Thm.string_of_thm thms) |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
126 |
| _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
127 |
in [((i, msg), id)] end) |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
128 |
and sorted_msgs context exn = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59056
diff
changeset
|
129 |
sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn)); |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
130 |
|
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
131 |
in sorted_msgs NONE e end; |
38874
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
132 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
133 |
end; |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
134 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
135 |
fun exn_messages exn = map #1 (exn_messages_ids exn); |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
136 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
137 |
fun exn_message exn = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
138 |
(case exn_messages exn of |
38875
c7a66b584147
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38874
diff
changeset
|
139 |
[] => "Interrupt" |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
140 |
| msgs => cat_lines (map snd msgs)); |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
141 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
142 |
val exn_error_message = Output.error_message o exn_message; |
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
57831
diff
changeset
|
143 |
val exn_system_message = Output.system_message o exn_message; |
62505 | 144 |
fun exn_trace e = Exn.trace exn_message tracing e; |
145 |
fun exn_trace_system e = Exn.trace exn_message Output.system_message e; |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
146 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
147 |
|
62498 | 148 |
(* exception debugger *) |
149 |
||
150 |
local |
|
151 |
||
152 |
fun print_entry (name, loc) = |
|
153 |
Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of loc)); |
|
154 |
||
155 |
fun exception_debugger output e = |
|
156 |
let |
|
157 |
val (trace, result) = Exn_Debugger.capture_exception_trace e; |
|
158 |
val _ = |
|
159 |
(case (trace, result) of |
|
160 |
(_ :: _, Exn.Exn exn) => |
|
161 |
output (cat_lines ("Exception trace - " ^ exn_message exn :: map print_entry trace)) |
|
162 |
| _ => ()); |
|
163 |
in Exn.release result end; |
|
164 |
||
165 |
in |
|
166 |
||
167 |
fun exn_debugger e = exception_debugger tracing e; |
|
168 |
fun exn_debugger_system e = exception_debugger Output.system_message e; |
|
169 |
||
170 |
end; |
|
171 |
||
172 |
||
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
173 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
174 |
(** controlled execution **) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
175 |
|
62498 | 176 |
fun debugging1 opt_context f x = |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
177 |
if ML_Options.exception_trace_enabled opt_context |
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
58894
diff
changeset
|
178 |
then exn_trace (fn () => f x) else f x; |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
179 |
|
62498 | 180 |
fun debugging2 opt_context f x = |
181 |
if ML_Options.exception_debugger_enabled opt_context |
|
182 |
then exn_debugger (fn () => f x) else f x; |
|
183 |
||
184 |
fun debugging opt_context f = |
|
185 |
f |> debugging1 opt_context |> debugging2 opt_context; |
|
186 |
||
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
187 |
fun controlled_execution opt_context f x = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
188 |
(f |> debugging opt_context |> Future.interruptible_task) x; |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
189 |
|
39238
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
190 |
fun toplevel_error output_exn f x = f x |
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
191 |
handle exn => |
62505 | 192 |
if Exn.is_interrupt exn then Exn.reraise exn |
39238
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
193 |
else |
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
194 |
let |
45197
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
195 |
val opt_ctxt = |
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
196 |
(case Context.thread_data () of |
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
197 |
NONE => NONE |
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
198 |
| SOME context => try Context.proof_of context); |
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
199 |
val _ = output_exn (exn_context opt_ctxt exn); |
39238
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
200 |
in raise TOPLEVEL_ERROR end; |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
201 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
202 |
fun toplevel_program body = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
203 |
(body |> controlled_execution NONE |> toplevel_error exn_error_message) (); |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
204 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
205 |
end; |