more precise treatment of exception nesting and serial numbers;

--- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:53:32 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 18:07:40 2011 +0200
@@ -9,7 +9,7 @@
 sig
   val serial: exn -> serial * exn
   val make: exn list -> exn
-  val dest: exn -> (serial * exn) list option
+  val dest: exn -> exn list option
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list
 end;
@@ -43,7 +43,7 @@
     [] => Exn.Interrupt
   | es => Par_Exn es);
 
-fun dest (Par_Exn exns) = SOME (map (`the_serial) exns)
+fun dest (Par_Exn exns) = SOME exns
   | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
 
 

--- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 18:07:40 2011 +0200
@@ -61,7 +61,7 @@
       | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
       | flatten context exn =
           (case Par_Exn.dest exn of
-            SOME exns => map (pair context) exns
+            SOME exns => maps (flatten context) exns
           | NONE => [(context, Par_Exn.serial exn)]);
 
     fun exn_msgs (context, (i, exn)) =
@@ -98,7 +98,7 @@
             | _ => 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));
+        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;
 

--- a/src/Pure/PIDE/document.ML	Thu Aug 18 17:53:32 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 18 18:07:40 2011 +0200
@@ -264,8 +264,8 @@
 fun run int tr st =
   (case Toplevel.transition int tr st of
     SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME exn_info) =>
-      (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+  | SOME (_, SOME (exn, _)) =>
+      (case ML_Compiler.exn_messages exn of
         [] => Exn.interrupt ()
       | errs => (errs, NONE))
   | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));