# HG changeset patch
# User wenzelm
# Date 1685522211 -7200
# Node ID 9609085da9695342c2c6975a201b602c3fb2caf9
# Parent  26b31f4029485c333641f02ad5f0f8258b23d567
more NEWS;

diff -r 26b31f402948 -r 9609085da969 NEWS
--- a/NEWS	Wed May 31 10:21:35 2023 +0200
+++ b/NEWS	Wed May 31 10:36:51 2023 +0200
@@ -361,6 +361,25 @@
 
 *** System ***
 
+* System options "context_theory_tracing" and "context_proof_tracing"
+store information about persistent context values (ML types theory,
+local_theory, Proof.context). This may reveal "memory leaks" in
+Isabelle/ML infrastructure or user tools, typically due to the lack of
+Thm.trim_context when thm values are stored as theory data.
+
+Below is a minimal example for Isabelle/ZF. The idea is to build a clean
+heap image with the above options enabled, and inspect the resulting ML
+heap later:
+
+  isabelle build -o context_theory_tracing -o context_proof_tracing -b -c ZF
+  isabelle process -l ZF -e "Session.print_context_tracing (K true)"
+
+An alternative to "isabelle process -l ZF" is "isabelle jedit -l ZF"
+with the subsequent ML snippets in an arbitrary theory context:
+
+  ML_command \<open>Session.print_context_tracing (K true)\<close>
+  ML \<open>Context.finish_tracing ()\<close>
+
 * The "rsync" tool has been bundled as Isabelle component, with uniform
 version and compilation options on all platforms. This allows to use
 more recent options for extra robustness, notably "--secluded-args"