changeset 54649 | 99b9249b3e05 |
parent 54647 | 7a8512d6206d |
child 54671 | d64a4ef26edb |
--- a/src/Pure/PIDE/command.ML Mon Nov 25 21:36:10 2013 +0100 +++ b/src/Pure/PIDE/command.ML Thu Nov 28 12:54:39 2013 +0100 @@ -63,7 +63,7 @@ val res = (body |> restore_attributes - |> Future.worker_context "Command.memo_exec" group + |> Future.task_context "Command.memo_exec" group |> Exn.interruptible_capture) (); in SOME ((), Result res) end else SOME ((), expr)