avoid excessive accumulation of garbage, for profiling of huge sessions;

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