# HG changeset patch
# User wenzelm
# Date 1721295369 -7200
# Node ID 9a40ec7a202796024da642402b101be3caf86735
# Parent  1bc7eef961ff78f5864e17fe429edf9a749d6c5c
more operations;

diff -r 1bc7eef961ff -r 9a40ec7a2027 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Jul 18 11:02:08 2024 +0200
+++ b/src/Pure/General/table.ML	Thu Jul 18 11:36:09 2024 +0200
@@ -66,7 +66,7 @@
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
-  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit}
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
   val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
 end;
 
@@ -592,7 +592,7 @@
 
 (* cache *)
 
-type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit};
+type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
 
 fun unsynchronized_cache f =
   let
@@ -609,7 +609,8 @@
                 Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
               | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))));
     fun reset () = (cache2 := empty; cache1 := empty);
-  in {apply = apply, reset = reset} end;
+    fun total_size () = size (! cache1) + size (! cache2);
+  in {apply = apply, reset = reset, size = total_size} end;
 
 
 (* ML pretty-printing *)
diff -r 1bc7eef961ff -r 9a40ec7a2027 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Thu Jul 18 11:02:08 2024 +0200
+++ b/src/Pure/term_items.ML	Thu Jul 18 11:36:09 2024 +0200
@@ -34,7 +34,7 @@
   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
-  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit};
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
   val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
   type set = int table
   val add_set: key -> set -> set
diff -r 1bc7eef961ff -r 9a40ec7a2027 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jul 18 11:02:08 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jul 18 11:36:09 2024 +0200
@@ -254,6 +254,7 @@
   val typ_of_tvar: indexname * sort -> typ
   val typ_of: ztyp -> typ
   val reset_cache: theory -> theory
+  val check_cache: theory -> {ztyp: int, typ: int} option
   val ztyp_cache: theory -> typ -> ztyp
   val typ_cache: theory -> ztyp -> typ
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
@@ -633,6 +634,10 @@
     SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); thy)
   | NONE => thy);
 
+fun check_cache thy =
+  Data.get thy
+  |> Option.map (fn (cache1, cache2) => {ztyp = #size cache1 (), typ = #size cache2 ()});
+
 fun ztyp_cache thy =
   (case Data.get thy of
     SOME (cache, _) => cache