1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jan 31 21:54:49 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jan 31 22:57:01 2011 +0100
     1.3 @@ -44,7 +44,8 @@
     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: {group: group option, deps: task list, pri: int} -> (unit -> 'a) list -> 'a future list
     1.8 +  val bulk: {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    val join_results: 'a future list -> 'a Exn.result list
    1.13 @@ -399,7 +400,7 @@
    1.14  
    1.15  (* fork *)
    1.16  
    1.17 -fun bulk {group, deps, pri} es =
    1.18 +fun bulk {name, group, deps, pri} es =
    1.19    let
    1.20      val grp =
    1.21        (case group of
    1.22 @@ -408,7 +409,7 @@
    1.23      fun enqueue e (minimal, queue) =
    1.24        let
    1.25          val (result, job) = future_job grp e;
    1.26 -        val ((task, minimal'), queue') = Task_Queue.enqueue grp deps pri job queue;
    1.27 +        val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
    1.28          val future = Future {promised = false, task = task, group = grp, result = result};
    1.29        in (future, (minimal orelse minimal', queue')) end;
    1.30    in
    1.31 @@ -423,7 +424,7 @@
    1.32        in futures end)
    1.33    end;
    1.34  
    1.35 -fun fork_pri pri e = singleton (bulk {group = NONE, deps = [], pri = pri}) e;
    1.36 +fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
    1.37  fun fork e = fork_pri 0 e;
    1.38  
    1.39  
    1.40 @@ -499,7 +500,9 @@
    1.41    in
    1.42      if extended then Future {promised = false, task = task, group = group, result = result}
    1.43      else
    1.44 -      singleton (bulk {group = SOME group, deps = [task], pri = Task_Queue.pri_of_task task})
    1.45 +      singleton
    1.46 +        (bulk {name = "Future.map", group = SOME group,
    1.47 +          deps = [task], pri = Task_Queue.pri_of_task task})
    1.48          (fn () => f (join x))
    1.49    end;
    1.50