# HG changeset patch
# User blanchet
# Date 1256662399 -3600
# Node ID 107f3df799f698580a444826b065667ed79b260e
# Parent  cba22e2999d5d2620966339a98baadeb60f48957
clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak

diff -r cba22e2999d5 -r 107f3df799f6 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Oct 27 16:52:06 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 27 17:53:19 2009 +0100
@@ -2398,11 +2398,11 @@
 & \textit{subgoal}\end{aligned}$
 \postw
 
+\let\antiq=\textrm
+
 \subsection{Registration of Coinductive Datatypes}
 \label{registration-of-coinductive-datatypes}
 
-\let\antiq=\textrm
-
 If you have defined a custom coinductive datatype, you can tell Nitpick about
 it, so that it can use an efficient Kodkod axiomatization similar to the one it
 uses for lazy lists. The interface for registering and unregistering coinductive
diff -r cba22e2999d5 -r 107f3df799f6 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 16:52:06 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 17:53:19 2009 +0100
@@ -1606,6 +1606,7 @@
                                  (tac ctxt (auto_tac (clasimpset_of ctxt))))
        #> the #> Goal.finish ctxt) goal
 
+val max_cached_wfs = 100
 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
 val cached_wf_props : (term * bool) list Unsynchronized.ref =
   Unsynchronized.ref []
@@ -1639,8 +1640,11 @@
                  else
                    ()
        in
-         if tac_timeout = (!cached_timeout) then ()
-         else (cached_wf_props := []; cached_timeout := tac_timeout);
+         if tac_timeout = (!cached_timeout)
+            andalso length (!cached_wf_props) < max_cached_wfs then
+           ()
+         else
+           (cached_wf_props := []; cached_timeout := tac_timeout);
          case AList.lookup (op =) (!cached_wf_props) prop of
            SOME wf => wf
          | NONE =>