diff -r a96d43a54650 -r afdbec23b92b src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Feb 02 18:22:13 2011 +0100 +++ b/src/Pure/Concurrent/future.ML Wed Feb 02 20:32:50 2011 +0100 @@ -440,12 +440,12 @@ else res); fun join_next deps = (*requires SYNCHRONIZED*) - if Task_Queue.finished_deps deps then NONE + if null deps then NONE else (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of - (NONE, deps') => - if Task_Queue.finished_deps deps' then NONE - else (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps') + (NONE, []) => NONE + | (NONE, deps') => + (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps') | (SOME work, deps') => SOME (work, deps')); fun execute_work NONE = () @@ -461,8 +461,7 @@ if forall is_finished xs then () else if Multithreading.self_critical () then error "Cannot join future values within critical section" - else if is_some (worker_task ()) then - join_work (Task_Queue.init_deps (map task_of xs)) + else if is_some (worker_task ()) then join_work (map task_of xs) else List.app (ignore o Single_Assignment.await o result_of) xs; in map get_result xs end; @@ -533,8 +532,8 @@ (Task_Queue.dequeue_passive (Thread.self ()) task)); in if still_passive then execute (task, [job]) else () end); val _ = - worker_waiting (Task_Queue.init_deps [task]) - (fn () => Single_Assignment.await result); + if is_some (Single_Assignment.peek result) then () + else worker_waiting [task] (fn () => ignore (Single_Assignment.await result)); in () end; fun fulfill x res = fulfill_result x (Exn.Result res);