# 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