equal
deleted
inserted
replaced
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; |