# HG changeset patch
# User wenzelm
# Date 1375100337 -7200
# Node ID 260949bf6529d3bfc9d6fb795845d2af8c6c923a
# Parent  dc13552494a27f812b8a88a87b63157b9c5b5dcc
actually purge removed goal futures -- avoid memory leak;

diff -r dc13552494a2 -r 260949bf6529 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Jul 29 13:43:43 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Jul 29 14:18:57 2013 +0200
@@ -49,6 +49,7 @@
 
         val (removed, assign_update, state') = Document.update old_id new_id edits state;
         val _ = List.app Execution.terminate removed;
+        val _ = Goal.purge_futures removed;
         val _ = List.app Isabelle_Process.reset_tracing removed;
 
         val _ =
diff -r dc13552494a2 -r 260949bf6529 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jul 29 13:43:43 2013 +0200
+++ b/src/Pure/goal.ML	Mon Jul 29 14:18:57 2013 +0200
@@ -27,6 +27,7 @@
   val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: int -> unit future list
+  val purge_futures: int list -> unit
   val reset_futures: unit -> Future.group list
   val shutdown_futures: unit -> unit
   val skip_proofs_enabled: unit -> bool
@@ -180,6 +181,14 @@
 fun peek_futures id =
   map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
 
+fun purge_futures ids =
+  Synchronized.change forked_proofs (fn (_, tab) =>
+    let
+      val tab' = fold Inttab.delete_safe ids tab;
+      val n' = Inttab.fold (Integer.add o length o #2) tab' 0;
+      val _ = Future.forked_proofs := n';
+    in (n', tab') end);
+
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (_, tab) =>
     let