--- a/src/Pure/Concurrent/future.ML Mon Nov 11 16:40:07 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Wed Nov 20 22:10:45 2013 +0100
@@ -48,8 +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
+ val worker_context: string -> group -> ('a -> 'b) -> 'a -> 'b
type 'a future
val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
@@ -110,13 +109,8 @@
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"
- else setmp_worker_task (Task_Queue.new_task group name NONE) f x;
+fun worker_context name group f x =
+ setmp_worker_task (Task_Queue.new_task group name NONE) f x;
fun worker_joining e =
(case worker_task () of