1.1 --- a/src/Pure/Concurrent/future.ML	Mon Sep 28 09:47:32 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Sep 28 12:09:18 2009 +0200
     1.3 @@ -37,10 +37,11 @@
     1.4    val peek: 'a future -> 'a Exn.result option
     1.5    val is_finished: 'a future -> bool
     1.6    val value: 'a -> 'a future
     1.7 -  val fork: (unit -> 'a) -> 'a future
     1.8    val fork_group: group -> (unit -> 'a) -> 'a future
     1.9 +  val fork_deps_pri: 'b future list -> int -> (unit -> 'a) -> 'a future
    1.10    val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
    1.11    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.12 +  val fork: (unit -> 'a) -> 'a future
    1.13    val join_results: 'a future list -> 'a Exn.result list
    1.14    val join_result: 'a future -> 'a Exn.result
    1.15    val join: 'a future -> 'a
    1.16 @@ -322,10 +323,11 @@
    1.17        in task end);
    1.18    in Future {task = task, group = group, result = result} end;
    1.19  
    1.20 -fun fork e = fork_future NONE [] 0 e;
    1.21  fun fork_group group e = fork_future (SOME group) [] 0 e;
    1.22 -fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
    1.23 -fun fork_pri pri e = fork_future NONE [] pri e;
    1.24 +fun fork_deps_pri deps pri e = fork_future NONE (map task_of deps) pri e;
    1.25 +fun fork_deps deps e = fork_deps_pri deps 0 e;
    1.26 +fun fork_pri pri e = fork_deps_pri [] pri e;
    1.27 +fun fork e = fork_deps [] e;
    1.28  
    1.29  
    1.30  (* join *)