# HG changeset patch
# User wenzelm
# Date 1536342566 -7200
# Node ID fc5763d000e817a9813f1161bc97d6d941456241
# Parent  19ddfe546620d228ffe47aa252fa5222b79a147d
proper tast_context (amending 5f44ad150ed8);

diff -r 19ddfe546620 -r fc5763d000e8 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Sep 07 19:27:28 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Sep 07 19:49:26 2018 +0200
@@ -452,7 +452,7 @@
 fun run_process execution_id exec_id process =
   let val group = Future.worker_subgroup () in
     if Execution.running execution_id exec_id [group] then
-      ignore (task_context group Lazy.force_result {strict = true} process)
+      ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ())
     else ()
   end;