proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
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_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
20 structure Runtime: RUNTIME =
27 exception EXCURSION_FAIL of exn * string;
28 exception TOPLEVEL_ERROR;
33 exception CONTEXT of Proof.context * exn;
35 fun exn_context NONE exn = exn
36 | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
41 fun if_context NONE _ _ = []
42 | if_context (SOME ctxt) f xs = map (f ctxt) xs;
44 fun exn_message exn_position e =
46 fun raised exn name msgs =
47 let val pos = Position.str_of (exn_position exn) in
49 [] => "exception " ^ name ^ " raised" ^ pos
50 | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
51 | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
54 val detailed = ! Output.debugging;
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 ::
73 if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
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 Display.string_of_thm thms else []))
79 | exn_msg _ exn = raised exn (General.exnMessage exn) [];
80 in exn_msg NONE e end;
84 (** controlled execution **)
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))
94 fun controlled_execution f =
97 |> Future.interruptible_task;
99 fun toplevel_error exn_message f x =
100 let val ctxt = Option.map Context.proof_of (Context.thread_data ()) in
102 (Output.error_msg (exn_message (exn_context ctxt exn));
103 raise TOPLEVEL_ERROR)