1.1 --- a/src/Pure/Concurrent/future.ML	Sat Aug 20 09:42:34 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Aug 20 15:52:29 2011 +0200
     1.3 @@ -62,12 +62,13 @@
     1.4    val fork: (unit -> 'a) -> 'a future
     1.5    val join_results: 'a future list -> 'a Exn.result list
     1.6    val join_result: 'a future -> 'a Exn.result
     1.7 +  val joins: 'a future list -> 'a list
     1.8    val join: 'a future -> 'a
     1.9    val join_tasks: task list -> unit
    1.10    val value_result: 'a Exn.result -> 'a future
    1.11    val value: 'a -> 'a future
    1.12 +  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.13    val map: ('a -> 'b) -> 'a future -> 'b future
    1.14 -  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.15    val promise_group: group -> (unit -> unit) -> 'a future
    1.16    val promise: (unit -> unit) -> 'a future
    1.17    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.18 @@ -534,6 +535,7 @@
    1.19  end;
    1.20  
    1.21  fun join_result x = singleton join_results x;
    1.22 +fun joins xs = Par_Exn.release_all (join_results xs);
    1.23  fun join x = Exn.release (join_result x);
    1.24  
    1.25  fun join_tasks [] = ()
    1.26 @@ -556,6 +558,10 @@
    1.27  
    1.28  fun value x = value_result (Exn.Res x);
    1.29  
    1.30 +fun cond_forks args es =
    1.31 +  if Multithreading.enabled () then forks args es
    1.32 +  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
    1.33 +
    1.34  fun map_future f x =
    1.35    let
    1.36      val task = task_of x;
    1.37 @@ -569,16 +575,12 @@
    1.38    in
    1.39      if extended then Future {promised = false, task = task, result = result}
    1.40      else
    1.41 -      (singleton o forks)
    1.42 +      (singleton o cond_forks)
    1.43          {name = "map_future", group = SOME group, deps = [task],
    1.44            pri = Task_Queue.pri_of_task task, interrupts = true}
    1.45          (fn () => f (join x))
    1.46    end;
    1.47  
    1.48 -fun cond_forks args es =
    1.49 -  if Multithreading.enabled () then forks args es
    1.50 -  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
    1.51 -
    1.52  
    1.53  (* promised futures -- fulfilled by external means *)
    1.54