# HG changeset patch
# User wenzelm
# Date 1222532287 -7200
# Node ID 3c5b4f636159ab06a3f0a9010fd3892cb96e9087
# Parent  a97fa342540d341ba5c1370d62c2fae2491fb970
moved release_results to future.ML;
get_some: simplified via Future.release_results;

diff -r a97fa342540d -r 3c5b4f636159 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Sat Sep 27 18:18:06 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Sat Sep 27 18:18:07 2008 +0200
@@ -17,7 +17,6 @@
 
 signature PAR_LIST =
 sig
-  val release_results: 'a Exn.result list -> 'a list
   val map: ('a -> 'b) -> 'a list -> 'b list
   val get_some: ('a -> 'b option) -> 'a list -> 'b option
   val find_some: ('a -> bool) -> 'a list -> 'a option
@@ -28,29 +27,12 @@
 structure ParList: PAR_LIST =
 struct
 
-(* release results *)
-
-fun proper_exn (Exn.Result _) = NONE
-  | proper_exn (Exn.Exn Interrupt) = NONE
-  | proper_exn (Exn.Exn exn) = SOME exn;
-
-fun release_results results =
-  (case get_first proper_exn results of
-    SOME exn => raise exn
-  | NONE => List.map Exn.release results);
-
-
-(* map *)
-
 fun raw_map f xs =
   let val group = TaskQueue.new_group () in
     Future.join_results (List.map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs)
   end;
 
-fun map f xs = release_results (raw_map f xs);
-
-
-(* get_some etc. *)
+fun map f xs = Future.release_results (raw_map f xs);
 
 fun get_some f xs =
   let
@@ -61,13 +43,7 @@
   in
     (case get_first found results of
       SOME y => SOME y
-    | NONE =>
-        (case get_first proper_exn results of
-          SOME exn => raise exn
-        | NONE =>
-            (case get_first Exn.get_exn results of
-              SOME exn => raise exn
-            | NONE => NONE)))
+    | NONE => (Future.release_results results; NONE))
   end;
 
 fun find_some P = get_some (fn x => if P x then SOME x else NONE);