1.1 --- a/src/Pure/Concurrent/future.ML	Thu Dec 04 23:02:56 2008 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Dec 04 23:46:20 2008 +0100
     1.3 @@ -30,14 +30,15 @@
     1.4    val enabled: unit -> bool
     1.5    type task = TaskQueue.task
     1.6    type group = TaskQueue.group
     1.7 -  val thread_data: unit -> (string * task * group) option
     1.8 +  val thread_data: unit -> (string * task) option
     1.9    type 'a future
    1.10    val task_of: 'a future -> task
    1.11    val group_of: 'a future -> group
    1.12    val peek: 'a future -> 'a Exn.result option
    1.13    val is_finished: 'a future -> bool
    1.14 -  val future: group option -> task list -> bool -> (unit -> 'a) -> 'a future
    1.15    val fork: (unit -> 'a) -> 'a future
    1.16 +  val fork_group: group -> (unit -> 'a) -> 'a future
    1.17 +  val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
    1.18    val fork_background: (unit -> 'a) -> 'a future
    1.19    val join_results: 'a future list -> 'a Exn.result list
    1.20    val join_result: 'a future -> 'a Exn.result
    1.21 @@ -64,7 +65,7 @@
    1.22  type task = TaskQueue.task;
    1.23  type group = TaskQueue.group;
    1.24  
    1.25 -local val tag = Universal.tag () : (string * task * group) option Universal.tag in
    1.26 +local val tag = Universal.tag () : (string * task) option Universal.tag in
    1.27    fun thread_data () = the_default NONE (Thread.getLocal tag);
    1.28    fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
    1.29  end;
    1.30 @@ -141,7 +142,7 @@
    1.31  fun execute name (task, group, run) =
    1.32    let
    1.33      val _ = trace_active ();
    1.34 -    val ok = setmp_thread_data (name, task, group) run ();
    1.35 +    val ok = setmp_thread_data (name, task) run ();
    1.36      val _ = SYNCHRONIZED "execute" (fn () =>
    1.37       (change queue (TaskQueue.finish task);
    1.38        if ok then ()
    1.39 @@ -247,10 +248,10 @@
    1.40        change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
    1.41    in Future {task = task, group = group, result = result} end;
    1.42  
    1.43 -fun fork_common pri = future (Option.map #3 (thread_data ())) [] pri;
    1.44 -
    1.45 -fun fork e = fork_common true e;
    1.46 -fun fork_background e = fork_common false e;
    1.47 +fun fork e = future NONE [] true e;
    1.48 +fun fork_group group e = future (SOME group) [] true e;
    1.49 +fun fork_deps deps e = future NONE (map task_of deps) true e;
    1.50 +fun fork_background e = future NONE [] false e;
    1.51  
    1.52  
    1.53  (* join: retrieve results *)
    1.54 @@ -275,7 +276,7 @@
    1.55                (*alien thread -- refrain from contending for resources*)
    1.56                while exists (not o is_finished) xs
    1.57                do SYNCHRONIZED "join_thread" (fn () => wait "join_thread")
    1.58 -          | SOME (name, task, _) =>
    1.59 +          | SOME (name, task) =>
    1.60                (*proper task -- actively work towards results*)
    1.61                let
    1.62                  val unfinished = xs |> map_filter
    1.63 @@ -293,12 +294,11 @@
    1.64  fun join_result x = singleton join_results x;
    1.65  fun join x = Exn.release (join_result x);
    1.66  
    1.67 +fun map f x = fork_deps [x] (fn () => f (join x));
    1.68 +
    1.69  
    1.70  (* misc operations *)
    1.71  
    1.72 -(*map: dependent fork/join*)
    1.73 -fun map f x = future (SOME (group_of x)) [task_of x] true (fn () => f (join x));
    1.74 -
    1.75  (*focus: collection of high-priority task*)
    1.76  fun focus tasks = SYNCHRONIZED "focus" (fn () =>
    1.77    change queue (TaskQueue.focus tasks));