# HG changeset patch
# User wenzelm
# Date 1690365595 -7200
# Node ID 12af46f2cd9405295ec65f179d1d373061d36fcb
# Parent  c956b43749f0210e708441c8a3fbb81c937d6f0e
avoid excessive accumulation of garbage, for profiling of huge sessions;

diff -r c956b43749f0 -r 12af46f2cd94 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jul 25 16:30:14 2023 +0200
+++ b/src/Pure/context.ML	Wed Jul 26 11:59:55 2023 +0200
@@ -204,8 +204,12 @@
 
 local
 
+val m = Integer.pow 18 2;
+
 fun cons_tokens var token =
-  Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens));
+  Synchronized.change var (fn (n, tokens) =>
+    let val tokens' = if n mod m = 0 then filter Unsynchronized.weak_active tokens else tokens
+    in (n + 1, Weak.weak (SOME token) :: tokens') end);
 
 fun finish_tokens var =
   Synchronized.change_result var (fn (n, tokens) =>