# HG changeset patch
# User wenzelm
# Date 1301171284 -3600
# Node ID eb84d28961a99ce84066c40a97a55a2755720a41
# Parent  8223e7f4b0dae35e1b118a7d187e6b796ce4b199
added Future.cond_forks convenience;

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 *)