explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
1.1 --- a/src/Pure/Isar/runtime.ML Wed Jun 09 15:09:00 2010 +0200
1.2 +++ b/src/Pure/Isar/runtime.ML Wed Jun 09 16:23:00 2010 +0200
1.3 @@ -54,6 +54,7 @@
1.4 val detailed = ! Output.debugging;
1.5
1.6 fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
1.7 + | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
1.8 | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
1.9 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
1.10 exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)