proper tast_context (amending 5f44ad150ed8);
authorwenzelm
Fri Sep 07 19:49:26 2018 +0200 (9 months ago)
changeset 68931fc5763d000e8
parent 68930 19ddfe546620
child 68932 e609c3dec6f8
proper tast_context (amending 5f44ad150ed8);
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Sep 07 19:27:28 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Sep 07 19:49:26 2018 +0200
     1.3 @@ -452,7 +452,7 @@
     1.4  fun run_process execution_id exec_id process =
     1.5    let val group = Future.worker_subgroup () in
     1.6      if Execution.running execution_id exec_id [group] then
     1.7 -      ignore (task_context group Lazy.force_result {strict = true} process)
     1.8 +      ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ())
     1.9      else ()
    1.10    end;
    1.11