equal
deleted
inserted
replaced
265 (* print exceptions *) |
265 (* print exceptions *) |
266 |
266 |
267 local |
267 local |
268 |
268 |
269 fun with_context f xs = |
269 fun with_context f xs = |
270 (case Context.get_context () of NONE => [] |
270 (case ML_Context.get_context () of NONE => [] |
271 | SOME context => map (f (Context.proof_of context)) xs); |
271 | SOME context => map (f (Context.proof_of context)) xs); |
272 |
272 |
273 fun raised name [] = "exception " ^ name ^ " raised" |
273 fun raised name [] = "exception " ^ name ^ " raised" |
274 | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg |
274 | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg |
275 | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); |
275 | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); |