1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jan 31 22:57:01 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jan 31 23:02:53 2011 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4    val group_of: 'a future -> group
     1.5    val peek: 'a future -> 'a Exn.result option
     1.6    val is_finished: 'a future -> bool
     1.7 -  val bulk: {name: string, group: group option, deps: task list, pri: int} ->
     1.8 +  val forks: {name: string, group: group option, deps: task list, pri: int} ->
     1.9      (unit -> 'a) list -> 'a future list
    1.10    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.11    val fork: (unit -> 'a) -> 'a future
    1.12 @@ -400,31 +400,33 @@
    1.13  
    1.14  (* fork *)
    1.15  
    1.16 -fun bulk {name, group, deps, pri} es =
    1.17 -  let
    1.18 -    val grp =
    1.19 -      (case group of
    1.20 -        NONE => worker_subgroup ()
    1.21 -      | SOME grp => grp);
    1.22 -    fun enqueue e (minimal, queue) =
    1.23 -      let
    1.24 -        val (result, job) = future_job grp e;
    1.25 -        val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
    1.26 -        val future = Future {promised = false, task = task, group = grp, result = result};
    1.27 -      in (future, (minimal orelse minimal', queue')) end;
    1.28 -  in
    1.29 -    SYNCHRONIZED "enqueue" (fn () =>
    1.30 -      let
    1.31 -        val (futures, minimal) =
    1.32 -          Unsynchronized.change_result queue (fn q =>
    1.33 -            let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
    1.34 -            in ((futures, minimal), q') end);
    1.35 -        val _ = if minimal then signal work_available else ();
    1.36 -        val _ = scheduler_check ();
    1.37 -      in futures end)
    1.38 -  end;
    1.39 +fun forks {name, group, deps, pri} es =
    1.40 +  if null es then []
    1.41 +  else
    1.42 +    let
    1.43 +      val grp =
    1.44 +        (case group of
    1.45 +          NONE => worker_subgroup ()
    1.46 +        | SOME grp => grp);
    1.47 +      fun enqueue e (minimal, queue) =
    1.48 +        let
    1.49 +          val (result, job) = future_job grp e;
    1.50 +          val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
    1.51 +          val future = Future {promised = false, task = task, group = grp, result = result};
    1.52 +        in (future, (minimal orelse minimal', queue')) end;
    1.53 +    in
    1.54 +      SYNCHRONIZED "enqueue" (fn () =>
    1.55 +        let
    1.56 +          val (futures, minimal) =
    1.57 +            Unsynchronized.change_result queue (fn q =>
    1.58 +              let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
    1.59 +              in ((futures, minimal), q') end);
    1.60 +          val _ = if minimal then signal work_available else ();
    1.61 +          val _ = scheduler_check ();
    1.62 +        in futures end)
    1.63 +    end;
    1.64  
    1.65 -fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
    1.66 +fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
    1.67  fun fork e = fork_pri 0 e;
    1.68  
    1.69  
    1.70 @@ -501,7 +503,7 @@
    1.71      if extended then Future {promised = false, task = task, group = group, result = result}
    1.72      else
    1.73        singleton
    1.74 -        (bulk {name = "Future.map", group = SOME group,
    1.75 +        (forks {name = "Future.map", group = SOME group,
    1.76            deps = [task], pri = Task_Queue.pri_of_task task})
    1.77          (fn () => f (join x))
    1.78    end;