--- 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