more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;

--- a/src/Pure/Isar/runtime.ML	Mon Aug 30 14:56:27 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Mon Aug 30 15:09:20 2010 +0200
@@ -11,6 +11,7 @@
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
   val exn_context: Proof.context option -> exn -> exn
+  val exn_messages: (exn -> Position.T) -> exn -> string list
   val exn_message: (exn -> Position.T) -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
   val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -41,7 +42,7 @@
 fun if_context NONE _ _ = []
   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
 
-fun exn_message exn_position e =
+fun exn_messages exn_position e =
   let
     fun raised exn name msgs =
       let val pos = Position.str_of (exn_position exn) in
@@ -53,32 +54,36 @@
 
     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)
-      | exn_msg _ TERMINATE = "Exit."
-      | exn_msg _ Exn.Interrupt = "Interrupt."
-      | exn_msg _ TimeLimit.TimeOut = "Timeout."
-      | exn_msg _ TOPLEVEL_ERROR = "Error."
-      | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
-      | exn_msg _ (ERROR msg) = msg
-      | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
-      | exn_msg _ (exn as THEORY (msg, thys)) =
-          raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
-      | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
-            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
-      | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
+    fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
+      | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
+      | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
+          map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
+      | exn_msgs _ TERMINATE = ["Exit."]
+      | exn_msgs _ Exn.Interrupt = []
+      | exn_msgs _ TimeLimit.TimeOut = ["Timeout."]
+      | exn_msgs _ TOPLEVEL_ERROR = ["Error."]
+      | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
+      | exn_msgs _ (ERROR msg) = [msg]
+      | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
+      | exn_msgs _ (exn as THEORY (msg, thys)) =
+          [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+      | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
+            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+      | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
             (if detailed then
               if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
-             else []))
-      | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
-            (if detailed then if_context ctxt Syntax.string_of_term ts else []))
-      | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
-            (if detailed then if_context ctxt Display.string_of_thm thms else []))
-      | exn_msg _ exn = raised exn (General.exnMessage exn) [];
-  in exn_msg NONE e end;
+             else []))]
+      | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
+            (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
+      | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
+            (if detailed then if_context ctxt Display.string_of_thm thms else []))]
+      | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
+  in exn_msgs NONE e end;
+
+fun exn_message exn_position exn =
+  (case exn_messages exn_position exn of
+    [] => "Interrupt."
+  | msgs => cat_lines msgs);
 
 
 

--- a/src/Pure/ML/ml_compiler.ML	Mon Aug 30 14:56:27 2010 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 30 15:09:20 2010 +0200
@@ -7,6 +7,7 @@
 signature ML_COMPILER =
 sig
   val exn_position: exn -> Position.T
+  val exn_messages: exn -> string list
   val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
@@ -15,6 +16,7 @@
 struct
 
 fun exn_position _ = Position.none;
+val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 
 fun eval verbose pos toks =

--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Aug 30 14:56:27 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Aug 30 15:09:20 2010 +0200
@@ -4,13 +4,6 @@
 Advanced runtime compilation for Poly/ML 5.3.0.
 *)
 
-signature ML_COMPILER =
-sig
-  val exn_position: exn -> Position.T
-  val exn_message: exn -> string
-  val eval: bool -> Position.T -> ML_Lex.token list -> unit
-end
-
 structure ML_Compiler: ML_COMPILER =
 struct
 
@@ -37,6 +30,7 @@
     NONE => Position.none
   | SOME loc => position_of loc);
 
+val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 
 

--- a/src/Pure/ROOT.ML	Mon Aug 30 14:56:27 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 30 15:09:20 2010 +0200
@@ -179,9 +179,9 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
+use "ML/ml_compiler.ML";
 if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
-  String.isPrefix "smlnj" ml_system
-then use "ML/ml_compiler.ML"
+  String.isPrefix "smlnj" ml_system then ()
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";