equal
deleted
inserted
replaced
11 exception TOPLEVEL_ERROR |
11 exception TOPLEVEL_ERROR |
12 val pretty_exn: exn -> Pretty.T |
12 val pretty_exn: exn -> Pretty.T |
13 val exn_context: Proof.context option -> exn -> exn |
13 val exn_context: Proof.context option -> exn -> exn |
14 val thread_context: exn -> exn |
14 val thread_context: exn -> exn |
15 type error = ((serial * string) * string option) |
15 type error = ((serial * string) * string option) |
16 val exn_messages_ids: exn -> error list |
16 val exn_messages: exn -> error list |
17 val exn_messages: exn -> (serial * string) list |
17 val exn_message_list: exn -> string list |
18 val exn_message: exn -> string |
18 val exn_message: exn -> string |
19 val exn_error_message: exn -> unit |
19 val exn_error_message: exn -> unit |
20 val exn_system_message: exn -> unit |
20 val exn_system_message: exn -> unit |
21 val exn_trace: (unit -> 'a) -> 'a |
21 val exn_trace: (unit -> 'a) -> 'a |
22 val exn_trace_system: (unit -> 'a) -> 'a |
22 val exn_trace_system: (unit -> 'a) -> 'a |
89 |
89 |
90 val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy; |
90 val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy; |
91 |
91 |
92 in |
92 in |
93 |
93 |
94 fun exn_messages_ids e = |
94 fun exn_messages e = |
95 let |
95 let |
96 fun raised exn name msgs = |
96 fun raised exn name msgs = |
97 let val pos = Position.here (Exn_Properties.position exn) in |
97 let val pos = Position.here (Exn_Properties.position exn) in |
98 (case msgs of |
98 (case msgs of |
99 [] => "exception " ^ name ^ " raised" ^ pos |
99 [] => "exception " ^ name ^ " raised" ^ pos |
139 |
139 |
140 in sorted_msgs NONE e end; |
140 in sorted_msgs NONE e end; |
141 |
141 |
142 end; |
142 end; |
143 |
143 |
144 fun exn_messages exn = map #1 (exn_messages_ids exn); |
144 fun exn_message_list exn = |
145 |
|
146 fun exn_message exn = |
|
147 (case exn_messages exn of |
145 (case exn_messages exn of |
148 [] => "Interrupt" |
146 [] => ["Interrupt"] |
149 | msgs => cat_lines (map snd msgs)); |
147 | msgs => map (#2 o #1) msgs); |
|
148 |
|
149 val exn_message = cat_lines o exn_message_list; |
150 |
150 |
151 val exn_error_message = Output.error_message o exn_message; |
151 val exn_error_message = Output.error_message o exn_message; |
152 val exn_system_message = Output.system_message o exn_message; |
152 val exn_system_message = Output.system_message o exn_message; |
153 fun exn_trace e = Exn.trace exn_message tracing e; |
153 fun exn_trace e = Exn.trace exn_message tracing e; |
154 fun exn_trace_system e = Exn.trace exn_message Output.system_message e; |
154 fun exn_trace_system e = Exn.trace exn_message Output.system_message e; |