equal
deleted
inserted
replaced
271 val detailed = ! debug; |
271 val detailed = ! debug; |
272 |
272 |
273 fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn |
273 fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn |
274 | exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns) |
274 | exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns) |
275 | exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg]) |
275 | exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg]) |
276 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = exn_msg ctxt exn ^ |
276 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = |
277 Output.escape (Markup.enclose Markup.location (Output.output ("\n" ^ loc))) |
277 exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) |
278 | exn_msg _ TERMINATE = "Exit." |
278 | exn_msg _ TERMINATE = "Exit." |
279 | exn_msg _ RESTART = "Restart." |
279 | exn_msg _ RESTART = "Restart." |
280 | exn_msg _ Interrupt = "Interrupt." |
280 | exn_msg _ Interrupt = "Interrupt." |
281 | exn_msg _ TimeLimit.TimeOut = "Timeout." |
281 | exn_msg _ TimeLimit.TimeOut = "Timeout." |
282 | exn_msg _ TOPLEVEL_ERROR = "Error." |
282 | exn_msg _ TOPLEVEL_ERROR = "Error." |