src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Sat Aug 20 09:42:34 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Aug 20 15:52:29 2011 +0200
@@ -62,12 +62,13 @@
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
+  val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
   val join_tasks: task list -> unit
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
+  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val promise_group: group -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -534,6 +535,7 @@
 end;
 
 fun join_result x = singleton join_results x;
+fun joins xs = Par_Exn.release_all (join_results xs);
 fun join x = Exn.release (join_result x);
 
 fun join_tasks [] = ()
@@ -556,6 +558,10 @@
 
 fun value x = value_result (Exn.Res x);
 
+fun cond_forks args es =
+  if Multithreading.enabled () then forks args es
+  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+
 fun map_future f x =
   let
     val task = task_of x;
@@ -569,16 +575,12 @@
   in
     if extended then Future {promised = false, task = task, result = result}
     else
-      (singleton o forks)
+      (singleton o cond_forks)
         {name = "map_future", group = SOME group, deps = [task],
           pri = Task_Queue.pri_of_task task, interrupts = true}
         (fn () => f (join x))
   end;
 
-fun cond_forks args es =
-  if Multithreading.enabled () then forks args es
-  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
-
 
 (* promised futures -- fulfilled by external means *)