clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
--- 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;