author | wenzelm |
Mon, 30 Aug 2010 15:09:20 +0200 | |
changeset 38874 | 4a4d34d2f97b |
parent 37370 | 582780d89e64 |
child 38875 | c7a66b584147 |
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 |
38874
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
14 |
val exn_messages: (exn -> Position.T) -> exn -> string list |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
15 |
val exn_message: (exn -> Position.T) -> exn -> string |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
16 |
val debugging: ('a -> 'b) -> 'a -> 'b |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
17 |
val controlled_execution: ('a -> 'b) -> 'a -> 'b |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
32091
diff
changeset
|
18 |
val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
19 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
20 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
21 |
structure Runtime: RUNTIME = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
22 |
struct |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
23 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
24 |
(** exceptions **) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
25 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
26 |
exception UNDEF; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
27 |
exception TERMINATE; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
28 |
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
|
29 |
exception TOPLEVEL_ERROR; |
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 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
32 |
(* exn_context *) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
33 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
34 |
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
|
35 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
36 |
fun exn_context NONE exn = exn |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
37 |
| exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn); |
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_message *) |
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 |
fun if_context NONE _ _ = [] |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
43 |
| if_context (SOME ctxt) f xs = map (f ctxt) xs; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
44 |
|
38874
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
45 |
fun exn_messages exn_position e = |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
46 |
let |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
47 |
fun raised exn name msgs = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
48 |
let val pos = Position.str_of (exn_position exn) in |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
49 |
(case msgs of |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
50 |
[] => "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
|
51 |
| [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
52 |
| _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
53 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
54 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
55 |
val detailed = ! Output.debugging; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
56 |
|
38874
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
57 |
fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
58 |
| exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
59 |
| exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) = |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
60 |
map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn) |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
61 |
| exn_msgs _ TERMINATE = ["Exit."] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
62 |
| exn_msgs _ Exn.Interrupt = [] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
63 |
| exn_msgs _ TimeLimit.TimeOut = ["Timeout."] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
64 |
| exn_msgs _ TOPLEVEL_ERROR = ["Error."] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
65 |
| exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
66 |
| exn_msgs _ (ERROR msg) = [msg] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
67 |
| exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
68 |
| exn_msgs _ (exn as THEORY (msg, thys)) = |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
69 |
[raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
70 |
| exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg :: |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
71 |
(if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
72 |
| exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg :: |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
73 |
(if detailed then |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
74 |
if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts |
38874
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
75 |
else []))] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
76 |
| exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg :: |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
77 |
(if detailed then if_context ctxt Syntax.string_of_term ts else []))] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
78 |
| exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg :: |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
79 |
(if detailed then if_context ctxt Display.string_of_thm thms else []))] |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
80 |
| exn_msgs _ exn = [raised exn (General.exnMessage exn) []]; |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
81 |
in exn_msgs NONE e end; |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
82 |
|
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
83 |
fun exn_message exn_position exn = |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
84 |
(case exn_messages exn_position exn of |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
85 |
[] => "Interrupt." |
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
37370
diff
changeset
|
86 |
| msgs => cat_lines msgs); |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
87 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
88 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
89 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
90 |
(** controlled execution **) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
91 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
92 |
fun debugging f x = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
93 |
if ! Output.debugging then |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
94 |
Exn.release (exception_trace (fn () => |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
95 |
Exn.Result (f x) handle |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
96 |
exn as UNDEF => Exn.Exn exn |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
97 |
| exn as EXCURSION_FAIL _ => Exn.Exn exn)) |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
98 |
else f x; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
99 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
100 |
fun controlled_execution f = |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
101 |
f |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
102 |
|> debugging |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
103 |
|> Future.interruptible_task; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
104 |
|
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
32091
diff
changeset
|
105 |
fun toplevel_error output_exn f x = |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
32091
diff
changeset
|
106 |
let val ctxt = Option.map Context.proof_of (Context.thread_data ()) |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
32091
diff
changeset
|
107 |
in f x handle exn => (output_exn (exn_context ctxt exn); 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
|
108 |
|
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
109 |
end; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff
changeset
|
110 |