src/Pure/Isar/runtime.ML

--- a/src/Pure/Isar/runtime.ML	Wed Jan 16 20:40:50 2013 +0100
+++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 20:41:29 2013 +0100
@@ -12,6 +12,7 @@
   exception TOPLEVEL_ERROR
   val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
+  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) 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
@@ -42,22 +43,28 @@
 
 (* exn_message *)
 
+local
+
 fun if_context NONE _ _ = []
   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
 
-fun exn_messages exn_position e =
+fun identify exn =
   let
-    fun identify exn =
-      let val exn' = Par_Exn.identify [] exn
-      in (Par_Exn.the_serial exn', exn') end;
+    val exn' = Par_Exn.identify [] exn;
+    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
+  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
 
-    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 => maps (flatten context) exns
-          | NONE => [(context, identify exn)]);
+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 => maps (flatten context) exns
+      | NONE => [(context, identify exn)]);
 
+in
+
+fun exn_messages_ids exn_position e =
+  let
     fun raised exn name msgs =
       let val pos = Position.here (exn_position exn) in
         (case msgs of
@@ -66,10 +73,10 @@
         | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
       end;
 
-    fun exn_msgs (context, (i, exn)) =
+    fun exn_msgs (context, ((i, exn), id)) =
       (case exn of
         EXCURSION_FAIL (exn, loc) =>
-          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
             (sorted_msgs context exn)
       | _ =>
         let
@@ -94,12 +101,17 @@
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: if_context context Display.string_of_thm thms)
             | _ => raised exn (General.exnMessage exn) []);
-        in [(i, msg)] end)
+        in [((i, msg), id)] end)
       and sorted_msgs context exn =
-        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;
 
+end;
+
+fun exn_messages exn_position exn =
+  map #1 (exn_messages_ids exn_position exn);
+
 fun exn_message exn_position exn =
   (case exn_messages exn_position exn of
     [] => "Interrupt"