255 | exn_msg _ RESTART = "Restart." |
255 | exn_msg _ RESTART = "Restart." |
256 | exn_msg _ Interrupt = "Interrupt." |
256 | exn_msg _ Interrupt = "Interrupt." |
257 | exn_msg _ Output.TOPLEVEL_ERROR = "Error." |
257 | exn_msg _ Output.TOPLEVEL_ERROR = "Error." |
258 | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg |
258 | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg |
259 | exn_msg _ (ERROR msg) = msg |
259 | exn_msg _ (ERROR msg) = msg |
260 | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg] |
260 | exn_msg detailed (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg detailed) exns @ [msg]) |
261 | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg] |
261 | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg] |
262 | exn_msg false (THEORY (msg, _)) = msg |
262 | exn_msg false (THEORY (msg, _)) = msg |
263 | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys) |
263 | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys) |
264 | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg] |
264 | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg] |
265 | exn_msg true (Syntax.AST (msg, asts)) = |
265 | exn_msg true (Syntax.AST (msg, asts)) = |