1.1 --- a/src/Pure/PIDE/command.ML	Mon Nov 11 16:40:07 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Nov 20 22:10:45 2013 +0100
     1.3 @@ -57,15 +57,17 @@
     1.4        (case expr of
     1.5          Expr (exec_id, body) =>
     1.6            uninterruptible (fn restore_attributes => fn () =>
     1.7 -            if Execution.running execution_id exec_id [Future.the_worker_group ()] then
     1.8 -              let
     1.9 -                val res =
    1.10 -                  (body
    1.11 -                    |> restore_attributes
    1.12 -                    |> Future.worker_nest "Command.memo_exec"
    1.13 -                    |> Exn.interruptible_capture) ();
    1.14 -              in SOME ((), Result res) end
    1.15 -            else SOME ((), expr)) ()
    1.16 +            let val group = Future.worker_subgroup () in
    1.17 +              if Execution.running execution_id exec_id [group] then
    1.18 +                let
    1.19 +                  val res =
    1.20 +                    (body
    1.21 +                      |> restore_attributes
    1.22 +                      |> Future.worker_context "Command.memo_exec" group
    1.23 +                      |> Exn.interruptible_capture) ();
    1.24 +                in SOME ((), Result res) end
    1.25 +              else SOME ((), expr)
    1.26 +            end) ()
    1.27        | Result _ => SOME ((), expr)))
    1.28    |> (fn NONE => error "Conflicting command execution" | _ => ());
    1.29