# HG changeset patch
# User wenzelm
# Date 1384981845 -3600
# Node ID db3d3d99c69df03d9f699028e77655596de3aae9
# Parent  75623b4d625103698a6f09e86b51a8e3d3d799af
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
tuned signature;

diff -r 75623b4d6251 -r db3d3d99c69d src/Pure/Concurrent/future.ML
--- 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
diff -r 75623b4d6251 -r db3d3d99c69d src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Nov 11 16:40:07 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 20 22:10:45 2013 +0100
@@ -57,15 +57,17 @@
       (case expr of
         Expr (exec_id, body) =>
           uninterruptible (fn restore_attributes => fn () =>
-            if Execution.running execution_id exec_id [Future.the_worker_group ()] then
-              let
-                val res =
-                  (body
-                    |> restore_attributes
-                    |> Future.worker_nest "Command.memo_exec"
-                    |> Exn.interruptible_capture) ();
-              in SOME ((), Result res) end
-            else SOME ((), expr)) ()
+            let val group = Future.worker_subgroup () in
+              if Execution.running execution_id exec_id [group] then
+                let
+                  val res =
+                    (body
+                      |> restore_attributes
+                      |> Future.worker_context "Command.memo_exec" group
+                      |> Exn.interruptible_capture) ();
+                in SOME ((), Result res) end
+              else SOME ((), expr)
+            end) ()
       | Result _ => SOME ((), expr)))
   |> (fn NONE => error "Conflicting command execution" | _ => ());
 
diff -r 75623b4d6251 -r db3d3d99c69d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Nov 11 16:40:07 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Nov 20 22:10:45 2013 +0100
@@ -159,8 +159,8 @@
     NONE => raise Runtime.TERMINATE
   | SOME line => map (read_chunk channel) (space_explode "," line));
 
-fun worker_guest e =
-  Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
+fun worker_context e =
+  Future.worker_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
 
 in
 
@@ -168,7 +168,7 @@
   let val continue =
     (case read_command channel of
       [] => (Output.error_msg "Isabelle process: no input"; true)
-    | name :: args => (worker_guest (fn () => run_command name args); true))
+    | name :: args => (worker_context (fn () => run_command name args); true))
     handle Runtime.TERMINATE => false
       | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
   in