src/Pure/Isar/toplevel.ML
changeset 28443 de653f1ad78b
parent 28433 b3dab95f098f
child 28446 a01de3b3fa2e
equal deleted inserted replaced
28442:bd9573735bdd 28443:de653f1ad78b
   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]