# HG changeset patch
# User wenzelm
# Date 1422535853 -3600
# Node ID 6fab87db556c7723d1365e062afad7f9d3d1af56
# Parent  c21b65a6834bdbba69d9a78e413f30dcf24af1b0
ensure that running into older execution is interruptible (see also b91dc7ab3464);

diff -r c21b65a6834b -r 6fab87db556c src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jan 29 13:49:03 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Jan 29 13:50:53 2015 +0100
@@ -38,6 +38,12 @@
 
 (** main phases of execution **)
 
+fun task_context group f =
+  f
+  |> Future.interruptible_task
+  |> Future.task_context "Command.run_process" group;
+
+
 (* read *)
 
 type blob =
@@ -143,7 +149,9 @@
 val eval_running = Execution.is_running_exec o eval_exec_id;
 fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
 
-fun eval_result (Eval {eval_process, ...}) = Lazy.force eval_process;
+fun eval_result (Eval {eval_process, ...}) =
+  task_context (Future.worker_subgroup ()) Lazy.force eval_process;
+
 val eval_result_state = #state o eval_result;
 
 local
@@ -369,7 +377,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 (Future.task_context "Command.run_process" group Lazy.force_result process)
+      ignore (task_context group Lazy.force_result process)
     else ()
   end;