src/Pure/Concurrent/future.ML
changeset 32096 cb9adb13f892
parent 32095 ad4be204fdfe
child 32099 5382c93108db
equal deleted inserted replaced
32095:ad4be204fdfe 32096:cb9adb13f892
   322       val _ = scheduler_check "join check";
   322       val _ = scheduler_check "join check";
   323       val _ = Multithreading.self_critical () andalso
   323       val _ = Multithreading.self_critical () andalso
   324         error "Cannot join future values within critical section";
   324         error "Cannot join future values within critical section";
   325 
   325 
   326       val worker = is_worker ();
   326       val worker = is_worker ();
       
   327       val _ = if worker then join_deps (map task_of xs) else ();
       
   328 
   327       fun join_wait x =
   329       fun join_wait x =
   328         if SYNCHRONIZED "join_wait" (fn () =>
   330         if SYNCHRONIZED "join_wait" (fn () =>
   329           is_finished x orelse (if worker then worker_wait () else wait (); false))
   331           is_finished x orelse (if worker then worker_wait () else wait (); false))
   330         then () else join_wait x;
   332         then () else join_wait x;
   331 
       
   332       val _ = if worker then join_deps (map task_of xs) else ();
       
   333       val _ = List.app join_wait xs;
   333       val _ = List.app join_wait xs;
   334 
   334 
   335     in map get_result xs end) ();
   335     in map get_result xs end) ();
   336 
   336 
   337 end;
   337 end;