--- a/src/Pure/Concurrent/future.ML Mon Sep 28 09:47:32 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Sep 28 12:09:18 2009 +0200
@@ -37,10 +37,11 @@
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val value: 'a -> 'a future
- val fork: (unit -> 'a) -> 'a future
val fork_group: group -> (unit -> 'a) -> 'a future
+ val fork_deps_pri: 'b future list -> int -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
+ 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 join: 'a future -> 'a
@@ -322,10 +323,11 @@
in task end);
in Future {task = task, group = group, result = result} end;
-fun fork e = fork_future NONE [] 0 e;
fun fork_group group e = fork_future (SOME group) [] 0 e;
-fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
-fun fork_pri pri e = fork_future NONE [] pri e;
+fun fork_deps_pri deps pri e = fork_future NONE (map task_of deps) pri e;
+fun fork_deps deps e = fork_deps_pri deps 0 e;
+fun fork_pri pri e = fork_deps_pri [] pri e;
+fun fork e = fork_deps [] e;
(* join *)