1.1 --- a/src/Pure/Concurrent/future.ML Wed Feb 02 18:22:13 2011 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Wed Feb 02 20:32:50 2011 +0100
1.3 @@ -440,12 +440,12 @@
1.4 else res);
1.5
1.6 fun join_next deps = (*requires SYNCHRONIZED*)
1.7 - if Task_Queue.finished_deps deps then NONE
1.8 + if null deps then NONE
1.9 else
1.10 (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of
1.11 - (NONE, deps') =>
1.12 - if Task_Queue.finished_deps deps' then NONE
1.13 - else (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps')
1.14 + (NONE, []) => NONE
1.15 + | (NONE, deps') =>
1.16 + (worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps')
1.17 | (SOME work, deps') => SOME (work, deps'));
1.18
1.19 fun execute_work NONE = ()
1.20 @@ -461,8 +461,7 @@
1.21 if forall is_finished xs then ()
1.22 else if Multithreading.self_critical () then
1.23 error "Cannot join future values within critical section"
1.24 - else if is_some (worker_task ()) then
1.25 - join_work (Task_Queue.init_deps (map task_of xs))
1.26 + else if is_some (worker_task ()) then join_work (map task_of xs)
1.27 else List.app (ignore o Single_Assignment.await o result_of) xs;
1.28 in map get_result xs end;
1.29
1.30 @@ -533,8 +532,8 @@
1.31 (Task_Queue.dequeue_passive (Thread.self ()) task));
1.32 in if still_passive then execute (task, [job]) else () end);
1.33 val _ =
1.34 - worker_waiting (Task_Queue.init_deps [task])
1.35 - (fn () => Single_Assignment.await result);
1.36 + if is_some (Single_Assignment.peek result) then ()
1.37 + else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
1.38 in () end;
1.39
1.40 fun fulfill x res = fulfill_result x (Exn.Result res);