proper tast_context (amending 5f44ad150ed8);
authorwenzelm
Fri, 07 Sep 2018 19:49:26 +0200
changeset 68931 fc5763d000e8
parent 68930 19ddfe546620
child 68932 e609c3dec6f8
proper tast_context (amending 5f44ad150ed8);
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;