# HG changeset patch
# User wenzelm
# Date 1422479962 -3600
# Node ID b91dc7ab346409d637e92262ff12cbdac8a00a60
# Parent  c7eff4356885074043b910c427f51991ec8474b5
more robust protocol command: purge removed execs asynchronously, to remain reactive despite problems to cancel "Command.run_process" in a situation of overrunning non-terminating tasks (see also 59f1591a11cb);

diff -r c7eff4356885 -r b91dc7ab3464 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Jan 28 19:25:19 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Jan 28 22:19:22 2015 +0100
@@ -82,9 +82,12 @@
               end;
 
           val (removed, assign_update, state') = Document.update old_id new_id edits state;
-          val _ = List.app Execution.terminate removed;
-          val _ = Execution.purge removed;
-          val _ = List.app Isabelle_Process.reset_tracing removed;
+          val _ =
+            (singleton o Future.forks)
+             {name = "Document.update/remove", group = NONE,
+              deps = maps Future.group_snapshot (maps Execution.peek removed),
+              pri = 1, interrupts = false}
+             (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
 
           val _ =
             Output.protocol_message Markup.assign_update