--- a/src/Pure/Concurrent/future.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 29 18:59:58 2013 +0200
@@ -48,6 +48,7 @@
val worker_group: unit -> group option
val the_worker_group: unit -> group
val worker_subgroup: unit -> group
+ val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
type 'a future
val task_of: 'a future -> task
@@ -108,6 +109,9 @@
fun worker_subgroup () = new_group (worker_group ());
+fun worker_nest name f x =
+ setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
+
fun worker_guest name group f x =
if is_some (worker_task ()) then
raise Fail "Already running as worker thread"