changeset 37370 | 582780d89e64 |
parent 33603 | 3713a5208671 |
child 38874 | 4a4d34d2f97b |
--- a/src/Pure/Isar/runtime.ML Wed Jun 09 15:09:00 2010 +0200 +++ b/src/Pure/Isar/runtime.ML Wed Jun 09 16:23:00 2010 +0200 @@ -54,6 +54,7 @@ val detailed = ! Output.debugging; fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn + | exn_msg _ (Exn.EXCEPTIONS []) = "Exception." | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)