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)