src/Pure/Isar/runtime.ML

--- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -12,7 +12,7 @@
   exception TOPLEVEL_ERROR
   val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
-  val exn_messages: (exn -> Position.T) -> exn -> string list
+  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
   val exn_message: (exn -> Position.T) -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
   val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -57,47 +57,55 @@
 
     val detailed = ! debug;
 
-    fun exn_msgs context exn =
-      if Exn.is_interrupt exn then []
-      else
-        (case Par_Exn.dest exn of
-          SOME exns => maps (exn_msgs context) (rev exns)
-        | NONE =>
+    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
+      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
+      | flatten context exn =
+          (case Par_Exn.dest exn of
+            SOME exns => map (pair context) exns
+          | NONE => [(context, Par_Exn.serial exn)]);
+
+    fun exn_msgs (context, (i, exn)) =
+      (case exn of
+        EXCURSION_FAIL (exn, loc) =>
+          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+            (sorted_msgs context exn)
+      | _ =>
+        let
+          val msg =
             (case exn of
-              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
-            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
-            | EXCURSION_FAIL (exn, loc) =>
-                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
-                  (exn_msgs context exn)
-            | TERMINATE => ["Exit"]
-            | TimeLimit.TimeOut => ["Timeout"]
-            | TOPLEVEL_ERROR => ["Error"]
-            | ERROR msg => [msg]
-            | Fail msg => [raised exn "Fail" [msg]]
+              TERMINATE => "Exit"
+            | TimeLimit.TimeOut => "Timeout"
+            | TOPLEVEL_ERROR => "Error"
+            | ERROR msg => msg
+            | Fail msg => raised exn "Fail" [msg]
             | THEORY (msg, thys) =>
-                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+                raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
             | Ast.AST (msg, asts) =>
-                [raised exn "AST" (msg ::
-                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
+                raised exn "AST" (msg ::
+                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))
             | TYPE (msg, Ts, ts) =>
-                [raised exn "TYPE" (msg ::
+                raised exn "TYPE" (msg ::
                   (if detailed then
                     if_context context Syntax.string_of_typ Ts @
                     if_context context Syntax.string_of_term ts
-                   else []))]
+                   else []))
             | TERM (msg, ts) =>
-                [raised exn "TERM" (msg ::
-                  (if detailed then if_context context Syntax.string_of_term ts else []))]
+                raised exn "TERM" (msg ::
+                  (if detailed then if_context context Syntax.string_of_term ts else []))
             | THM (msg, i, thms) =>
-                [raised exn ("THM " ^ string_of_int i) (msg ::
-                  (if detailed then if_context context Display.string_of_thm thms else []))]
-            | _ => [raised exn (General.exnMessage exn) []]));
-  in exn_msgs NONE e end;
+                raised exn ("THM " ^ string_of_int i) (msg ::
+                  (if detailed then if_context context Display.string_of_thm thms else []))
+            | _ => raised exn (General.exnMessage exn) []);
+        in [(i, msg)] end)
+      and sorted_msgs context exn =
+        sort (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+
+  in sorted_msgs NONE e end;
 
 fun exn_message exn_position exn =
   (case exn_messages exn_position exn of
     [] => "Interrupt"
-  | msgs => cat_lines msgs);
+  | msgs => cat_lines (map snd msgs));
 
 
 (** controlled execution **)