1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 28 14:29:25 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 28 14:35:27 2009 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4    else if count_active () > Multithreading.max_threads_value () then
     1.5      (worker_wait scheduler_event; worker_next ())
     1.6    else
     1.7 -    (case change_result queue Task_Queue.dequeue of
     1.8 +    (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
     1.9        NONE => (worker_wait work_available; worker_next ())
    1.10      | some => some);
    1.11  
    1.12 @@ -346,7 +346,7 @@
    1.13  fun join_next deps = (*requires SYNCHRONIZED*)
    1.14    if null deps then NONE
    1.15    else
    1.16 -    (case change_result queue (Task_Queue.dequeue_towards deps) of
    1.17 +    (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
    1.18        (NONE, []) => NONE
    1.19      | (NONE, deps') => (worker_wait work_finished; join_next deps')
    1.20      | (SOME work, deps') => SOME (work, deps'));

     2.1 --- a/src/Pure/Concurrent/task_queue.ML	Tue Jul 28 14:29:25 2009 +0200
     2.2 +++ b/src/Pure/Concurrent/task_queue.ML	Tue Jul 28 14:35:27 2009 +0200
     2.3 @@ -26,8 +26,8 @@
     2.4    val cancel_all: queue -> group list
     2.5    val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
     2.6    val extend: task -> (bool -> bool) -> queue -> queue option
     2.7 -  val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
     2.8 -  val dequeue_towards: task list -> queue ->
     2.9 +  val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
    2.10 +  val dequeue_towards: Thread.thread -> task list -> queue ->
    2.11      (((task * group * (bool -> bool) list) option * task list) * queue)
    2.12    val finish: task -> queue -> bool * queue
    2.13  end;
    2.14 @@ -179,7 +179,7 @@
    2.15  
    2.16  (* dequeue *)
    2.17  
    2.18 -fun dequeue (queue as Queue {groups, jobs, cache}) =
    2.19 +fun dequeue thread (queue as Queue {groups, jobs, cache}) =
    2.20    let
    2.21      fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list)
    2.22        | ready _ = NONE;
    2.23 @@ -188,7 +188,7 @@
    2.24          NONE => (NONE, make_queue groups jobs No_Result)
    2.25        | SOME (result as (task, _, _)) =>
    2.26            let
    2.27 -            val jobs' = set_job task (Running (Thread.self ())) jobs;
    2.28 +            val jobs' = set_job task (Running thread) jobs;
    2.29              val cache' = Result task;
    2.30            in (SOME result, make_queue groups jobs' cache') end);
    2.31    in
    2.32 @@ -201,7 +201,7 @@
    2.33  
    2.34  (* dequeue_towards -- adhoc dependencies *)
    2.35  
    2.36 -fun dequeue_towards deps (queue as Queue {groups, jobs, ...}) =
    2.37 +fun dequeue_towards thread deps (queue as Queue {groups, jobs, ...}) =
    2.38    let
    2.39      fun ready task =
    2.40        (case Task_Graph.get_node jobs task of
    2.41 @@ -213,7 +213,7 @@
    2.42      val tasks = filter (can (Task_Graph.get_node jobs)) deps;
    2.43      fun result (res as (task, _, _)) =
    2.44        let
    2.45 -        val jobs' = set_job task (Running (Thread.self ())) jobs;
    2.46 +        val jobs' = set_job task (Running thread) jobs;
    2.47          val cache' = Unknown;
    2.48        in ((SOME res, tasks), make_queue groups jobs' cache') end;
    2.49    in