src/Pure/Isar/toplevel.ML
changeset 28458 0966ac3f4a40
parent 28453 06702e7acd1d
child 28463 b8f16c92122a
equal deleted inserted replaced
28457:25669513fd4c 28458:0966ac3f4a40
   256 fun exn_message e =
   256 fun exn_message e =
   257   let
   257   let
   258     val detailed = ! debug;
   258     val detailed = ! debug;
   259 
   259 
   260     fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
   260     fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
   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])
       
   263       | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
   262       | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
   264           exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
   263           exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
   265       | exn_msg _ TERMINATE = "Exit."
   264       | exn_msg _ TERMINATE = "Exit."
   266       | exn_msg _ Exn.Interrupt = "Interrupt."
   265       | exn_msg _ Exn.Interrupt = "Interrupt."
   267       | exn_msg _ TimeLimit.TimeOut = "Timeout."
   266       | exn_msg _ TimeLimit.TimeOut = "Timeout."