# HG changeset patch
# User wenzelm
# Date 1276093380 -7200
# Node ID 582780d89e64d0366b39c16384d569068d34e9f2
# Parent  e0460bbf6b39ffb389eefec9442077f402209f40
explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;

diff -r e0460bbf6b39 -r 582780d89e64 src/Pure/Isar/runtime.ML
--- 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)