1.1 --- a/src/Pure/Concurrent/future.ML	Thu Oct 01 16:09:47 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Oct 01 16:27:13 2009 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    type task = Task_Queue.task
     1.5    type group = Task_Queue.group
     1.6    val is_worker: unit -> bool
     1.7 +  val worker_task: unit -> Task_Queue.task option
     1.8    val worker_group: unit -> Task_Queue.group option
     1.9    type 'a future
    1.10    val task_of: 'a future -> task
    1.11 @@ -71,6 +72,7 @@
    1.12  end;
    1.13  
    1.14  val is_worker = is_some o thread_data;
    1.15 +val worker_task = Option.map #2 o thread_data;
    1.16  val worker_group = Option.map #3 o thread_data;
    1.17  
    1.18  
    1.19 @@ -347,7 +349,8 @@
    1.20    | SOME res => res);
    1.21  
    1.22  fun join_wait x =
    1.23 -  Synchronized.guarded_access (result_of x) (fn NONE => NONE | some => SOME ((), some));
    1.24 +  Synchronized.guarded_access (result_of x)
    1.25 +    (fn NONE => NONE | some => SOME ((), some));
    1.26  
    1.27  fun join_next deps = (*requires SYNCHRONIZED*)
    1.28    if null deps then NONE
    1.29 @@ -357,10 +360,14 @@
    1.30      | (NONE, deps') => (worker_wait work_finished; join_next deps')
    1.31      | (SOME work, deps') => SOME (work, deps'));
    1.32  
    1.33 -fun join_work deps =
    1.34 -  (case SYNCHRONIZED "join" (fn () => join_next deps) of
    1.35 -    NONE => ()
    1.36 -  | SOME (work, deps') => (execute "join" work; join_work deps'));
    1.37 +fun execute_work NONE = ()
    1.38 +  | execute_work (SOME (work, deps')) = (execute "join" work; join_work deps')
    1.39 +and join_work deps =
    1.40 +  execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
    1.41 +
    1.42 +fun join_depend task deps =
    1.43 +  execute_work (SYNCHRONIZED "join" (fn () =>
    1.44 +    (Unsynchronized.change queue (Task_Queue.depend task deps); join_next deps)));
    1.45  
    1.46  in
    1.47  
    1.48 @@ -368,11 +375,11 @@
    1.49    if forall is_finished xs then map get_result xs
    1.50    else if Multithreading.self_critical () then
    1.51      error "Cannot join future values within critical section"
    1.52 -  else uninterruptible (fn _ => fn () =>
    1.53 -     (if is_worker ()
    1.54 -      then join_work (map task_of xs)
    1.55 -      else List.app join_wait xs;
    1.56 -      map get_result xs)) ();
    1.57 +  else
    1.58 +    (case worker_task () of
    1.59 +      SOME task => join_depend task (map task_of xs)
    1.60 +    | NONE => List.app join_wait xs;
    1.61 +    map get_result xs);
    1.62  
    1.63  end;
    1.64