allow worker guest threads, which participate actively in future joins, but are outside thread accounting;

--- a/src/Pure/Concurrent/future.ML	Sun Jul 07 22:58:34 2013 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jul 08 12:00:45 2013 +0200
@@ -47,6 +47,7 @@
   val worker_task: unit -> task option
   val worker_group: unit -> group option
   val worker_subgroup: unit -> group
+  val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
   type 'a future
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
@@ -100,6 +101,11 @@
 val worker_group = Option.map Task_Queue.group_of_task o worker_task;
 fun worker_subgroup () = new_group (worker_group ());
 
+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_joining e =
   (case worker_task () of
     NONE => e ()
@@ -266,15 +272,12 @@
   in () end;
 
 fun worker_wait active cond = (*requires SYNCHRONIZED*)
-  let
-    val state =
-      (case AList.lookup Thread.equal (! workers) (Thread.self ()) of
-        SOME state => state
-      | NONE => raise Fail "Unregistered worker thread");
-    val _ = state := (if active then Waiting else Sleeping);
-    val _ = wait cond;
-    val _ = state := Working;
-  in () end;
+  (case AList.lookup Thread.equal (! workers) (Thread.self ()) of
+    SOME state =>
+     (state := (if active then Waiting else Sleeping);
+      wait cond;
+      state := Working)
+  | NONE => ignore (wait cond));
 
 fun worker_next () = (*requires SYNCHRONIZED*)
   if length (! workers) > ! max_workers then

--- a/src/Pure/Concurrent/task_queue.ML	Sun Jul 07 22:58:34 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jul 08 12:00:45 2013 +0200
@@ -17,6 +17,7 @@
   val str_of_groups: group -> string
   type task
   val dummy_task: task
+  val new_task: group -> string -> int option -> task
   val group_of_task: task -> group
   val name_of_task: task -> string
   val pri_of_task: task -> int