more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;
--- 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;