# HG changeset patch # User wenzelm # Date 1224600780 -7200 # Node ID 8068cdc84e7e925c89b1fa574e6747e490e946f3 # Parent 3a8d75c935ce150db2f9f88cf350ae4a27de65b2 join_results: allow CRITICAL join of finished futures; added singleton join_result; diff -r 3a8d75c935ce -r 8068cdc84e7e src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Tue Oct 21 16:52:59 2008 +0200 +++ b/src/Pure/Concurrent/future.ML Tue Oct 21 16:53:00 2008 +0200 @@ -40,6 +40,7 @@ val fork: (unit -> 'a) -> 'a T val fork_background: (unit -> 'a) -> 'a T val join_results: 'a T list -> 'a Exn.result list + val join_result: 'a T -> 'a Exn.result val join: 'a T -> 'a val focus: task list -> unit val interrupt_task: string -> unit @@ -258,6 +259,7 @@ let val _ = scheduler_check "join check"; val _ = Multithreading.self_critical () andalso + exists (not o is_finished) xs andalso error "Cannot join future values within critical section"; fun join_loop _ [] = () @@ -287,7 +289,8 @@ in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) (); -fun join x = Exn.release (singleton join_results x); +fun join_result x = singleton join_results x; +fun join x = Exn.release (join_result x); (* misc operations *)