|
1 (* Title: Pure/Isar/runtime.ML |
|
2 Author: Makarius |
|
3 |
|
4 Isar toplevel runtime support. |
|
5 *) |
|
6 |
|
7 signature RUNTIME = |
|
8 sig |
|
9 exception UNDEF |
|
10 exception TERMINATE |
|
11 exception EXCURSION_FAIL of exn * string |
|
12 exception TOPLEVEL_ERROR |
|
13 val exn_context: Proof.context option -> exn -> exn |
|
14 val exn_message: (exn -> Position.T) -> exn -> string |
|
15 val debugging: ('a -> 'b) -> 'a -> 'b |
|
16 val controlled_execution: ('a -> 'b) -> 'a -> 'b |
|
17 val toplevel_error: (exn -> string) -> ('a -> 'b) -> 'a -> 'b |
|
18 end; |
|
19 |
|
20 structure Runtime: RUNTIME = |
|
21 struct |
|
22 |
|
23 (** exceptions **) |
|
24 |
|
25 exception UNDEF; |
|
26 exception TERMINATE; |
|
27 exception EXCURSION_FAIL of exn * string; |
|
28 exception TOPLEVEL_ERROR; |
|
29 |
|
30 |
|
31 (* exn_context *) |
|
32 |
|
33 exception CONTEXT of Proof.context * exn; |
|
34 |
|
35 fun exn_context NONE exn = exn |
|
36 | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn); |
|
37 |
|
38 |
|
39 (* exn_message *) |
|
40 |
|
41 fun if_context NONE _ _ = [] |
|
42 | if_context (SOME ctxt) f xs = map (f ctxt) xs; |
|
43 |
|
44 fun exn_message exn_position e = |
|
45 let |
|
46 fun raised exn name msgs = |
|
47 let val pos = Position.str_of (exn_position exn) in |
|
48 (case msgs of |
|
49 [] => "exception " ^ name ^ " raised" ^ pos |
|
50 | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg |
|
51 | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) |
|
52 end; |
|
53 |
|
54 val detailed = ! Output.debugging; |
|
55 |
|
56 fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn |
|
57 | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) |
|
58 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = |
|
59 exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) |
|
60 | exn_msg _ TERMINATE = "Exit." |
|
61 | exn_msg _ Exn.Interrupt = "Interrupt." |
|
62 | exn_msg _ TimeLimit.TimeOut = "Timeout." |
|
63 | exn_msg _ TOPLEVEL_ERROR = "Error." |
|
64 | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg |
|
65 | exn_msg _ (ERROR msg) = msg |
|
66 | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg] |
|
67 | exn_msg _ (exn as THEORY (msg, thys)) = |
|
68 raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else [])) |
|
69 | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg :: |
|
70 (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else [])) |
|
71 | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg :: |
|
72 (if detailed then |
|
73 if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts |
|
74 else [])) |
|
75 | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg :: |
|
76 (if detailed then if_context ctxt Syntax.string_of_term ts else [])) |
|
77 | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg :: |
|
78 (if detailed then if_context ctxt ProofContext.string_of_thm thms else [])) |
|
79 | exn_msg _ exn = raised exn (General.exnMessage exn) []; |
|
80 in exn_msg NONE e end; |
|
81 |
|
82 |
|
83 |
|
84 (** controlled execution **) |
|
85 |
|
86 fun debugging f x = |
|
87 if ! Output.debugging then |
|
88 Exn.release (exception_trace (fn () => |
|
89 Exn.Result (f x) handle |
|
90 exn as UNDEF => Exn.Exn exn |
|
91 | exn as EXCURSION_FAIL _ => Exn.Exn exn)) |
|
92 else f x; |
|
93 |
|
94 fun controlled_execution f = |
|
95 f |
|
96 |> debugging |
|
97 |> Future.interruptible_task; |
|
98 |
|
99 fun toplevel_error exn_message f x = |
|
100 let val ctxt = Option.map Context.proof_of (Context.thread_data ()) in |
|
101 f x handle exn => |
|
102 (Output.error_msg (exn_message (exn_context ctxt exn)); |
|
103 raise TOPLEVEL_ERROR) |
|
104 end; |
|
105 |
|
106 end; |
|
107 |