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