tune Par_Exn.make: balance merge;
clarified Par_Exn.dest: later exceptions first;

--- a/Admin/polyml/future/ROOT.ML	Thu Aug 18 16:52:19 2011 +0900
+++ b/Admin/polyml/future/ROOT.ML	Thu Aug 18 15:15:43 2011 +0200
@@ -78,6 +78,7 @@
 use "General/table.ML";
 use "General/graph.ML";
 use "General/ord_list.ML";
+use "General/balanced_tree.ML";
 
 structure Position =
 struct

--- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 16:52:19 2011 +0900
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:15:43 2011 +0200
@@ -29,17 +29,19 @@
 
 (* parallel exceptions *)
 
-exception Par_Exn of exn Ord_List.T;
+exception Par_Exn of exn list;
+  (*non-empty list with unique identified elements sorted by exn_ord;
+    no occurrences of Par_Exn or Exn.Interrupt*)
 
-fun par_exns (Par_Exn exns) = SOME exns
-  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
+fun par_exns (Par_Exn exns) = exns
+  | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
 
 fun make exns =
-  (case map_filter par_exns exns of
+  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
     [] => Exn.Interrupt
-  | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
+  | es => Par_Exn es);
 
-fun dest (Par_Exn exns) = SOME (rev exns)
+fun dest (Par_Exn exns) = SOME exns
   | dest _ = NONE;
 
 

--- a/src/Pure/Isar/runtime.ML	Thu Aug 18 16:52:19 2011 +0900
+++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 15:15:43 2011 +0200
@@ -61,7 +61,7 @@
       if Exn.is_interrupt exn then []
       else
         (case Par_Exn.dest exn of
-          SOME exns => maps (exn_msgs context) exns
+          SOME exns => maps (exn_msgs context) (rev exns)
         | NONE =>
             (case exn of
               Exn.EXCEPTIONS exns => maps (exn_msgs context) exns