src/Pure/term.scala

--- a/src/Pure/term.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/term.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -133,17 +133,25 @@
 
   /** cache **/
 
-  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
-    new Cache(initial_size, max_string)
+  object Cache
+  {
+    def make(
+        max_string: Int = Integer.MAX_VALUE,
+        initial_size: Int = isabelle.Cache.default_initial_size): Cache =
+      new Cache(initial_size, max_string)
 
-  class Cache private[Term](initial_size: Int, max_string: Int)
-    extends isabelle.Cache(initial_size, max_string)
+    val none: Cache = make(max_string = 0)
+  }
+
+  class Cache private[Term](max_string: Int, initial_size: Int)
+    extends isabelle.Cache(max_string = max_string, initial_size = initial_size)
   {
     protected def cache_indexname(x: Indexname): Indexname =
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
 
     protected def cache_sort(x: Sort): Sort =
-      if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string))
+      if (x.isEmpty) Nil
+      else lookup(x) getOrElse store(x.map(cache_string))
 
     protected def cache_typ(x: Typ): Typ =
     {
@@ -216,13 +224,19 @@
     }
 
     // main methods
-    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
-    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
-    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
-    def term(x: Term): Term = synchronized { cache_term(x) }
-    def proof(x: Proof): Proof = synchronized { cache_proof(x) }
+    def indexname(x: Indexname): Indexname =
+      if (no_cache) x else synchronized { cache_indexname(x) }
+    def sort(x: Sort): Sort =
+      if (no_cache) x else synchronized { cache_sort(x) }
+    def typ(x: Typ): Typ =
+      if (no_cache) x else synchronized { cache_typ(x) }
+    def term(x: Term): Term =
+      if (no_cache) x else synchronized { cache_term(x) }
+    def proof(x: Proof): Proof =
+      if (no_cache) x else synchronized { cache_proof(x) }
 
     def position(x: Position.T): Position.T =
-      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
+      if (no_cache) x
+      else synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
   }
 }