src/Pure/Isar/toplevel.ML
changeset 26293 a71ea4a57f44
parent 26257 707969e76f5c
child 26491 c93ff30790fe
equal deleted inserted replaced
26292:009e56d16080 26293:a71ea4a57f44
   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."