src/Pure/Concurrent/future.ML
changeset 42566 afdbec23b92b
parent 42563 73dde8006820
child 42579 d2e6b1132df2
     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);