src/Pure/PIDE/command.ML
changeset 55298 99b9249b3e05
parent 55296 7a8512d6206d
child 56013 d64a4ef26edb
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Nov 25 21:36:10 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Nov 28 12:54:39 2013 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4                    val res =
     1.5                      (body
     1.6                        |> restore_attributes
     1.7 -                      |> Future.worker_context "Command.memo_exec" group
     1.8 +                      |> Future.task_context "Command.memo_exec" group
     1.9                        |> Exn.interruptible_capture) ();
    1.10                  in SOME ((), Result res) end
    1.11                else SOME ((), expr)