Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
authorwenzelm
Wed, 09 Jun 2010 16:23:00 +0200
changeset 37370 582780d89e64
parent 37369 e0460bbf6b39
child 37371 dced658407c4
explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
src/Pure/Isar/runtime.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle