# HG changeset patch # User wenzelm # Date 1373576036 -7200 # Node ID a44e9a1d5d8bf51fb566a2c0015d3677eead1593 # Parent 00170ef1dc39ffdf8a21247c384028f2c9676171 tuned signature; unified exceptions for this module; diff -r 00170ef1dc39 -r a44e9a1d5d8b src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Jul 11 18:41:05 2013 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Jul 11 22:53:56 2013 +0200 @@ -46,6 +46,7 @@ val new_group: group option -> group val worker_task: unit -> task option val worker_group: unit -> group option + val the_worker_group: unit -> group val worker_subgroup: unit -> group val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b type 'a future @@ -99,6 +100,12 @@ end; val worker_group = Option.map Task_Queue.group_of_task o worker_task; + +fun the_worker_group () = + (case worker_group () of + SOME group => group + | NONE => raise Fail "Missing worker thread context"); + fun worker_subgroup () = new_group (worker_group ()); fun worker_guest name group f x = @@ -556,7 +563,7 @@ val _ = if forall is_finished xs then () else if Multithreading.self_critical () then - error "Cannot join future values within critical section" + raise Fail "Cannot join future values within critical section" else if is_some (worker_task ()) then join_work (map task_of xs) else List.app (ignore o Single_Assignment.await o result_of) xs; in map get_result xs end;