# HG changeset patch
# User wenzelm
# Date 1313674740 -7200
# Node ID d9c7bf932eabc23f08a2645267670f888880739f
# Parent  b94951f06e48b52fc3c04f73dec566c7da392be6
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;

diff -r b94951f06e48 -r d9c7bf932eab src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:37:01 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:39:00 2011 +0200
@@ -47,19 +47,19 @@
 
 (* parallel results *)
 
-fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
+fun release_all results =
+  if forall (fn Exn.Res _ => true | _ => false) results
+  then map Exn.release results
+  else raise make (map_filter Exn.get_exn results);
 
-fun release_all results =
-  if all_res results then map Exn.release results
-  else raise make (map_filter Exn.get_exn results);
+fun plain_exn (Exn.Res _) = NONE
+  | plain_exn (Exn.Exn (Par_Exn _)) = NONE
+  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
 
 fun release_first results =
-  if all_res results then map Exn.release results
-  else
-    (case get_first
-        (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
-      NONE => Exn.interrupt ()
-    | SOME exn => reraise exn);
+  (case get_first plain_exn results of
+    NONE => release_all results
+  | SOME exn => reraise exn);
 
 end;