--- a/src/Pure/Concurrent/future.ML Sat Mar 26 18:31:39 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Sat Mar 26 21:28:04 2011 +0100
@@ -49,6 +49,9 @@
val join: 'a future -> 'a
val value: 'a -> 'a future
val map: ('a -> 'b) -> 'a future -> 'b future
+ val cond_forks:
+ {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
+ (unit -> 'a) list -> 'a future list
val promise_group: Task_Queue.group -> 'a future
val promise: unit -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -500,6 +503,10 @@
(fn () => f (join x))
end;
+fun cond_forks args es =
+ if Multithreading.enabled () then forks args es
+ else map (fn e => value (e ())) es;
+
(* promised futures -- fulfilled by external means *)