1.1 --- a/src/Pure/Concurrent/future.ML	Mon Nov 11 16:40:07 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Nov 20 22:10:45 2013 +0100
     1.3 @@ -48,8 +48,7 @@
     1.4    val worker_group: unit -> group option
     1.5    val the_worker_group: unit -> group
     1.6    val worker_subgroup: unit -> group
     1.7 -  val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
     1.8 -  val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
     1.9 +  val worker_context: string -> group -> ('a -> 'b) -> 'a -> 'b
    1.10    type 'a future
    1.11    val task_of: 'a future -> task
    1.12    val peek: 'a future -> 'a Exn.result option
    1.13 @@ -110,13 +109,8 @@
    1.14  
    1.15  fun worker_subgroup () = new_group (worker_group ());
    1.16  
    1.17 -fun worker_nest name f x =
    1.18 -  setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
    1.19 -
    1.20 -fun worker_guest name group f x =
    1.21 -  if is_some (worker_task ()) then
    1.22 -    raise Fail "Already running as worker thread"
    1.23 -  else setmp_worker_task (Task_Queue.new_task group name NONE) f x;
    1.24 +fun worker_context name group f x =
    1.25 +  setmp_worker_task (Task_Queue.new_task group name NONE) f x;
    1.26  
    1.27  fun worker_joining e =
    1.28    (case worker_task () of

     2.1 --- a/src/Pure/PIDE/command.ML	Mon Nov 11 16:40:07 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Nov 20 22:10:45 2013 +0100
     2.3 @@ -57,15 +57,17 @@
     2.4        (case expr of
     2.5          Expr (exec_id, body) =>
     2.6            uninterruptible (fn restore_attributes => fn () =>
     2.7 -            if Execution.running execution_id exec_id [Future.the_worker_group ()] then
     2.8 -              let
     2.9 -                val res =
    2.10 -                  (body
    2.11 -                    |> restore_attributes
    2.12 -                    |> Future.worker_nest "Command.memo_exec"
    2.13 -                    |> Exn.interruptible_capture) ();
    2.14 -              in SOME ((), Result res) end
    2.15 -            else SOME ((), expr)) ()
    2.16 +            let val group = Future.worker_subgroup () in
    2.17 +              if Execution.running execution_id exec_id [group] then
    2.18 +                let
    2.19 +                  val res =
    2.20 +                    (body
    2.21 +                      |> restore_attributes
    2.22 +                      |> Future.worker_context "Command.memo_exec" group
    2.23 +                      |> Exn.interruptible_capture) ();
    2.24 +                in SOME ((), Result res) end
    2.25 +              else SOME ((), expr)
    2.26 +            end) ()
    2.27        | Result _ => SOME ((), expr)))
    2.28    |> (fn NONE => error "Conflicting command execution" | _ => ());
    2.29  

     3.1 --- a/src/Pure/System/isabelle_process.ML	Mon Nov 11 16:40:07 2013 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Nov 20 22:10:45 2013 +0100
     3.3 @@ -159,8 +159,8 @@
     3.4      NONE => raise Runtime.TERMINATE
     3.5    | SOME line => map (read_chunk channel) (space_explode "," line));
     3.6  
     3.7 -fun worker_guest e =
     3.8 -  Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
     3.9 +fun worker_context e =
    3.10 +  Future.worker_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
    3.11  
    3.12  in
    3.13  
    3.14 @@ -168,7 +168,7 @@
    3.15    let val continue =
    3.16      (case read_command channel of
    3.17        [] => (Output.error_msg "Isabelle process: no input"; true)
    3.18 -    | name :: args => (worker_guest (fn () => run_command name args); true))
    3.19 +    | name :: args => (worker_context (fn () => run_command name args); true))
    3.20      handle Runtime.TERMINATE => false
    3.21        | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
    3.22    in