explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
1 (* Title: Pure/Isar/runtime.ML
4 Isar toplevel runtime support.
11 exception EXCURSION_FAIL of exn * string
12 exception TOPLEVEL_ERROR
13 val debug: bool Unsynchronized.ref
14 val exn_context: Proof.context option -> exn -> exn
15 val exn_messages: (exn -> Position.T) -> exn -> string list
16 val exn_message: (exn -> Position.T) -> exn -> string
17 val debugging: ('a -> 'b) -> 'a -> 'b
18 val controlled_execution: ('a -> 'b) -> 'a -> 'b
19 val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
22 structure Runtime: RUNTIME =
29 exception EXCURSION_FAIL of exn * string;
30 exception TOPLEVEL_ERROR;
32 val debug = Unsynchronized.ref false;
37 exception CONTEXT of Proof.context * exn;
39 fun exn_context NONE exn = exn
40 | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
45 fun if_context NONE _ _ = []
46 | if_context (SOME ctxt) f xs = map (f ctxt) xs;
48 fun exn_messages exn_position e =
50 fun raised exn name msgs =
51 let val pos = Position.str_of (exn_position exn) in
53 [] => "exception " ^ name ^ " raised" ^ pos
54 | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
55 | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
58 val detailed = ! debug;
60 fun exn_msgs context exn =
61 if Exn.is_interrupt exn then []
64 Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
65 | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
66 | EXCURSION_FAIL (exn, loc) =>
67 map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
68 | TERMINATE => ["Exit"]
69 | TimeLimit.TimeOut => ["Timeout"]
70 | TOPLEVEL_ERROR => ["Error"]
72 | Fail msg => [raised exn "Fail" [msg]]
73 | THEORY (msg, thys) =>
74 [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
75 | Syntax.AST (msg, asts) =>
76 [raised exn "AST" (msg ::
77 (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
78 | TYPE (msg, Ts, ts) =>
79 [raised exn "TYPE" (msg ::
81 if_context context Syntax.string_of_typ Ts @
82 if_context context Syntax.string_of_term ts
85 [raised exn "TERM" (msg ::
86 (if detailed then if_context context Syntax.string_of_term ts else []))]
87 | THM (msg, i, thms) =>
88 [raised exn ("THM " ^ string_of_int i) (msg ::
89 (if detailed then if_context context Display.string_of_thm thms else []))]
90 | _ => [raised exn (General.exnMessage exn) []]);
91 in exn_msgs NONE e end;
93 fun exn_message exn_position exn =
94 (case exn_messages exn_position exn of
96 | msgs => cat_lines msgs);
99 (** controlled execution **)
103 Exn.release (exception_trace (fn () =>
104 Exn.Result (f x) handle
105 exn as UNDEF => Exn.Exn exn
106 | exn as EXCURSION_FAIL _ => Exn.Exn exn))
109 fun controlled_execution f x =
110 ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
112 fun toplevel_error output_exn f x = f x
114 if Exn.is_interrupt exn then reraise exn
117 val ctxt = Option.map Context.proof_of (Context.thread_data ());
118 val _ = output_exn (exn_context ctxt exn);
119 in raise TOPLEVEL_ERROR end;