equal
deleted
inserted
replaced
261 | exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns) |
261 | exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns) |
262 | exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg]) |
262 | exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg]) |
263 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = |
263 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = |
264 exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) |
264 exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) |
265 | exn_msg _ TERMINATE = "Exit." |
265 | exn_msg _ TERMINATE = "Exit." |
266 | exn_msg _ Interrupt = "Interrupt." |
266 | exn_msg _ Exn.Interrupt = "Interrupt." |
267 | exn_msg _ TimeLimit.TimeOut = "Timeout." |
267 | exn_msg _ TimeLimit.TimeOut = "Timeout." |
268 | exn_msg _ TOPLEVEL_ERROR = "Error." |
268 | exn_msg _ TOPLEVEL_ERROR = "Error." |
269 | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg |
269 | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg |
270 | exn_msg _ (ERROR msg) = msg |
270 | exn_msg _ (ERROR msg) = msg |
271 | exn_msg _ (Fail msg) = raised "Fail" [msg] |
271 | exn_msg _ (Fail msg) = raised "Fail" [msg] |