author | wenzelm |
Fri, 15 Aug 2014 13:39:59 +0200 | |
changeset 57975 | c657c68a60ab |
parent 57831 | 885888a880fb |
child 58843 | 521cea5fa777 |
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 TERMINATE |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
11 |
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
|
12 |
exception TOPLEVEL_ERROR |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
13 |
val exn_context: Proof.context option -> 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 |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
21 |
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
|
22 |
val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
32091
diff
changeset
|
23 |
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
|
24 |
val toplevel_program: (unit -> 'a) -> 'a |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
25 |
val thread: bool -> (unit -> unit) -> Thread.thread |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
26 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
27 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
28 |
structure Runtime: RUNTIME = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
29 |
struct |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
30 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
31 |
(** exceptions **) |
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 |
exception UNDEF; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
34 |
exception TERMINATE; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
35 |
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
|
36 |
exception TOPLEVEL_ERROR; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
37 |
|
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 |
(* exn_context *) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
40 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
41 |
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
|
42 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
43 |
fun exn_context NONE exn = exn |
39285 | 44 |
| 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
|
45 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
46 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
47 |
(* exn_message *) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
48 |
|
51285 | 49 |
type error = ((serial * string) * string option); |
50 |
||
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
51 |
local |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
52 |
|
52686 | 53 |
fun robust f x = |
54 |
(case try f x of |
|
55 |
SOME s => s |
|
56 |
| NONE => Markup.markup Markup.intensify "<malformed>"); |
|
57 |
||
58 |
fun robust2 f x y = robust (fn () => f x y) (); |
|
59 |
||
60 |
fun robust_context NONE _ _ = [] |
|
61 |
| 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
|
62 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
63 |
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
|
64 |
let |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
70 |
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
|
71 |
| 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
|
72 |
| 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
|
73 |
(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
|
74 |
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
|
75 |
| 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
|
76 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
77 |
in |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
78 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
79 |
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
|
80 |
let |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
81 |
fun raised exn name msgs = |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
82 |
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
|
83 |
(case msgs of |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
84 |
[] => "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
|
85 |
| [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg |
51653 | 86 |
| _ => |
87 |
cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: |
|
88 |
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
|
89 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
90 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
91 |
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
|
92 |
(case exn of |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
93 |
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
|
94 |
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
|
95 |
(sorted_msgs context exn) |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
96 |
| _ => |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
97 |
let |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
98 |
val msg = |
44247 | 99 |
(case exn of |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
100 |
TERMINATE => "Exit" |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
101 |
| TimeLimit.TimeOut => "Timeout" |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
102 |
| 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
|
103 |
| ERROR "" => "Error" |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
104 |
| ERROR msg => msg |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
105 |
| Fail msg => raised exn "Fail" [msg] |
44247 | 106 |
| THEORY (msg, thys) => |
52686 | 107 |
raised exn "THEORY" (msg :: map (robust Context.str_of_thy) thys) |
44247 | 108 |
| Ast.AST (msg, asts) => |
52686 | 109 |
raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts) |
44247 | 110 |
| TYPE (msg, Ts, ts) => |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
111 |
raised exn "TYPE" (msg :: |
52686 | 112 |
(robust_context context Syntax.string_of_typ Ts @ |
113 |
robust_context context Syntax.string_of_term ts)) |
|
44247 | 114 |
| TERM (msg, ts) => |
52686 | 115 |
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
|
116 |
| CTERM (msg, cts) => |
d022e8bd2375
improved printing of exception CTERM (see also d0f0f37ec346);
wenzelm
parents:
51639
diff
changeset
|
117 |
raised exn "CTERM" |
52686 | 118 |
(msg :: robust_context context Syntax.string_of_term (map term_of cts)) |
44247 | 119 |
| 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
|
120 |
raised exn ("THM " ^ string_of_int i) |
52686 | 121 |
(msg :: robust_context context Display.string_of_thm thms) |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
122 |
| _ => 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
|
123 |
in [((i, msg), id)] end) |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
124 |
and sorted_msgs context exn = |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
125 |
sort_distinct (int_ord o pairself (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
|
126 |
|
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
127 |
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
|
128 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
129 |
end; |
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
130 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
131 |
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
|
132 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
133 |
fun exn_message exn = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
134 |
(case exn_messages exn of |
38875
c7a66b584147
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38874
diff
changeset
|
135 |
[] => "Interrupt" |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44264
diff
changeset
|
136 |
| 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
|
137 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
138 |
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
|
139 |
val exn_system_message = Output.system_message o exn_message; |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
140 |
fun exn_trace e = print_exception_trace exn_message e; |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
141 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
142 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
143 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
144 |
(** controlled execution **) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
145 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
146 |
fun debugging opt_context f x = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
147 |
if ML_Options.exception_trace_enabled opt_context |
53709
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
52686
diff
changeset
|
148 |
then print_exception_trace exn_message (fn () => f x) |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
149 |
else f x; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
150 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
151 |
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
|
152 |
(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
|
153 |
|
39238
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
154 |
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
|
155 |
handle exn => |
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
156 |
if Exn.is_interrupt exn then reraise exn |
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
157 |
else |
7189a138dd6c
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents:
39232
diff
changeset
|
158 |
let |
45197
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
159 |
val opt_ctxt = |
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
160 |
(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
|
161 |
NONE => NONE |
b6c527c64789
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents:
44295
diff
changeset
|
162 |
| 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
|
163 |
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
|
164 |
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
|
165 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
166 |
fun toplevel_program body = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
167 |
(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
|
168 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
169 |
(*Proof General legacy*) |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
170 |
fun thread interrupts body = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
171 |
Thread.fork |
57666
1c0ee733325f
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
wenzelm
parents:
56303
diff
changeset
|
172 |
(fn () => |
1c0ee733325f
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
wenzelm
parents:
56303
diff
changeset
|
173 |
debugging NONE body () handle exn => |
1c0ee733325f
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
wenzelm
parents:
56303
diff
changeset
|
174 |
if Exn.is_interrupt exn then () |
1c0ee733325f
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
wenzelm
parents:
56303
diff
changeset
|
175 |
else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn), |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
176 |
Simple_Thread.attributes interrupts); |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56279
diff
changeset
|
177 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
178 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
179 |