more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
1 (* Title: Pure/Isar/runtime.ML
4 Isar toplevel runtime support.
11 exception EXCURSION_FAIL of exn * string
12 exception TOPLEVEL_ERROR
13 val exn_context: Proof.context option -> exn -> exn
14 val exn_messages: (exn -> Position.T) -> exn -> string list
15 val exn_message: (exn -> Position.T) -> exn -> string
16 val debugging: ('a -> 'b) -> 'a -> 'b
17 val controlled_execution: ('a -> 'b) -> 'a -> 'b
18 val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
21 structure Runtime: RUNTIME =
28 exception EXCURSION_FAIL of exn * string;
29 exception TOPLEVEL_ERROR;
34 exception CONTEXT of Proof.context * exn;
36 fun exn_context NONE exn = exn
37 | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
42 fun if_context NONE _ _ = []
43 | if_context (SOME ctxt) f xs = map (f ctxt) xs;
45 fun exn_messages exn_position e =
47 fun raised exn name msgs =
48 let val pos = Position.str_of (exn_position exn) in
50 [] => "exception " ^ name ^ " raised" ^ pos
51 | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
52 | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
55 val detailed = ! Output.debugging;
57 fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
58 | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
59 | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
60 map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
61 | exn_msgs _ TERMINATE = ["Exit."]
62 | exn_msgs _ Exn.Interrupt = []
63 | exn_msgs _ TimeLimit.TimeOut = ["Timeout."]
64 | exn_msgs _ TOPLEVEL_ERROR = ["Error."]
65 | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
66 | exn_msgs _ (ERROR msg) = [msg]
67 | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
68 | exn_msgs _ (exn as THEORY (msg, thys)) =
69 [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
70 | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
71 (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
72 | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
74 if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
76 | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
77 (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
78 | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
79 (if detailed then if_context ctxt Display.string_of_thm thms else []))]
80 | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
81 in exn_msgs NONE e end;
83 fun exn_message exn_position exn =
84 (case exn_messages exn_position exn of
86 | msgs => cat_lines msgs);
90 (** controlled execution **)
93 if ! Output.debugging then
94 Exn.release (exception_trace (fn () =>
95 Exn.Result (f x) handle
96 exn as UNDEF => Exn.Exn exn
97 | exn as EXCURSION_FAIL _ => Exn.Exn exn))
100 fun controlled_execution f =
103 |> Future.interruptible_task;
105 fun toplevel_error output_exn f x =
106 let val ctxt = Option.map Context.proof_of (Context.thread_data ())
107 in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;