# HG changeset patch
# User wenzelm
# Date 1363266898 -3600
# Node ID 12e46440e3919f785de01416e2684d20179ce27e
# Parent  08bb002396528f988f2028e50a1a772105701d3c
more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;

diff -r 08bb00239652 -r 12e46440e391 src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Thu Mar 14 13:57:44 2013 +0100
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Mar 14 14:14:58 2013 +0100
@@ -19,7 +19,7 @@
 structure Par_Exn: PAR_EXN =
 struct
 
-(* identification via serial numbers *)
+(* identification via serial numbers -- NOT portable! *)
 
 fun identify default_props exn =
   let
@@ -46,9 +46,10 @@
   | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
 
 fun make exns =
-  (case Ord_List.unions exn_ord (map par_exns exns) of
-    [] => Exn.Interrupt
-  | es => Par_Exn es);
+  let
+    val exnss = map par_exns exns;
+    val exns' = Ord_List.unions exn_ord exnss handle Option.Option => flat exnss;
+  in if null exns' then Exn.Interrupt else Par_Exn exns' end;
 
 fun dest (Par_Exn exns) = SOME exns
   | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;