52 | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) |
52 | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) |
53 end; |
53 end; |
54 |
54 |
55 val detailed = ! Output.debugging; |
55 val detailed = ! Output.debugging; |
56 |
56 |
57 fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn |
57 fun exn_msgs context exn = |
58 | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns |
58 if Exn.is_interrupt exn then [] |
59 | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) = |
59 else |
60 map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn) |
60 (case exn of |
61 | exn_msgs _ TERMINATE = ["Exit"] |
61 Exn.EXCEPTIONS exns => maps (exn_msgs context) exns |
62 | exn_msgs _ Exn.Interrupt = [] |
62 | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn |
63 | exn_msgs _ TimeLimit.TimeOut = ["Timeout"] |
63 | EXCURSION_FAIL (exn, loc) => |
64 | exn_msgs _ TOPLEVEL_ERROR = ["Error"] |
64 map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn) |
65 | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg] |
65 | TERMINATE => ["Exit"] |
66 | exn_msgs _ (ERROR msg) = [msg] |
66 | TimeLimit.TimeOut => ["Timeout"] |
67 | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]] |
67 | TOPLEVEL_ERROR => ["Error"] |
68 | exn_msgs _ (exn as THEORY (msg, thys)) = |
68 | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg] |
69 [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))] |
69 | ERROR msg => [msg] |
70 | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg :: |
70 | Fail msg => [raised exn "Fail" [msg]] |
71 (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))] |
71 | THEORY (msg, thys) => |
72 | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg :: |
72 [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))] |
73 (if detailed then |
73 | Syntax.AST (msg, asts) => |
74 if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts |
74 [raised exn "AST" (msg :: |
75 else []))] |
75 (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))] |
76 | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg :: |
76 | TYPE (msg, Ts, ts) => |
77 (if detailed then if_context ctxt Syntax.string_of_term ts else []))] |
77 [raised exn "TYPE" (msg :: |
78 | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg :: |
78 (if detailed then |
79 (if detailed then if_context ctxt Display.string_of_thm thms else []))] |
79 if_context context Syntax.string_of_typ Ts @ |
80 | exn_msgs _ exn = [raised exn (General.exnMessage exn) []]; |
80 if_context context Syntax.string_of_term ts |
|
81 else []))] |
|
82 | TERM (msg, ts) => |
|
83 [raised exn "TERM" (msg :: |
|
84 (if detailed then if_context context Syntax.string_of_term ts else []))] |
|
85 | THM (msg, i, thms) => |
|
86 [raised exn ("THM " ^ string_of_int i) (msg :: |
|
87 (if detailed then if_context context Display.string_of_thm thms else []))] |
|
88 | _ => [raised exn (General.exnMessage exn) []]); |
81 in exn_msgs NONE e end; |
89 in exn_msgs NONE e end; |
82 |
90 |
83 fun exn_message exn_position exn = |
91 fun exn_message exn_position exn = |
84 (case exn_messages exn_position exn of |
92 (case exn_messages exn_position exn of |
85 [] => "Interrupt" |
93 [] => "Interrupt" |