--- a/src/Pure/Concurrent/par_exn.ML Fri Aug 31 22:34:37 2012 +0200
+++ b/src/Pure/Concurrent/par_exn.ML Sat Sep 01 19:27:28 2012 +0200
@@ -10,6 +10,7 @@
val serial: exn -> serial * exn
val make: exn list -> exn
val dest: exn -> exn list option
+ val is_interrupted: 'a Exn.result list -> bool
val release_all: 'a Exn.result list -> 'a list
val release_first: 'a Exn.result list -> 'a list
end;
@@ -53,6 +54,10 @@
(* parallel results *)
+fun is_interrupted results =
+ exists (fn Exn.Exn _ => true | _ => false) results andalso
+ Exn.is_interrupt (make (map_filter Exn.get_exn results));
+
fun release_all results =
if forall (fn Exn.Res _ => true | _ => false) results
then map Exn.release results