diff -r 8223e7f4b0da -r eb84d28961a9 src/Pure/Concurrent/future.ML --- 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 *)