clarified signature --- internal Cache.none;

--- a/src/Pure/Admin/build_log.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -244,7 +244,7 @@
 
     /* properties (YXML) */
 
-    val xml_cache: XML.Cache = XML.make_cache()
+    val xml_cache: XML.Cache = XML.Cache.make()
 
     def parse_props(text: String): Properties.T =
       try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) }
@@ -648,14 +648,14 @@
       errors = log_file.filter(Protocol.Error_Message_Marker))
   }
 
-  def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] =
+  def compress_errors(errors: List[String], cache: XZ.Cache = XZ.Cache()): Option[Bytes] =
     if (errors.isEmpty) None
     else {
       Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
         compress(cache = cache))
     }
 
-  def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] =
+  def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.Cache()): List[String] =
     if (bytes.is_empty) Nil
     else {
       XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text))
@@ -850,13 +850,16 @@
 
   /* database access */
 
-  def store(options: Options): Store = new Store(options)
+  def store(options: Options,
+      xml_cache: XML.Cache = XML.Cache.make(),
+      xz_cache: XZ.Cache = XZ.Cache.make()): Store =
+    new Store(options, xml_cache, xz_cache)
 
-  class Store private[Build_Log](options: Options)
+  class Store private[Build_Log](
+    options: Options,
+    val xml_cache: XML.Cache,
+    val xz_cache: XZ.Cache)
   {
-    val xml_cache: XML.Cache = XML.make_cache()
-    val xz_cache: XZ.Cache = XZ.make_cache()
-
     def open_database(
       user: String = options.string("build_log_database_user"),
       password: String = options.string("build_log_database_password"),
@@ -1164,7 +1167,7 @@
                 ml_statistics =
                   if (ml_statistics) {
                     Properties.uncompress(
-                      res.bytes(Data.ml_statistics), cache = xz_cache, Some(xml_cache))
+                      res.bytes(Data.ml_statistics), cache = xz_cache, xml_cache = xml_cache)
                   }
                   else Nil)
             session_name -> session_entry

--- a/src/Pure/General/bytes.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/General/bytes.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -195,17 +195,17 @@
 
   /* XZ data compression */
 
-  def uncompress(cache: XZ.Cache = XZ.cache()): Bytes =
+  def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
     using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
 
-  def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes =
+  def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes =
   {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 
-  def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache())
+  def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache())
     : (Boolean, Bytes) =
   {
     val compressed = compress(options = options, cache = cache)

--- a/src/Pure/General/cache.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/General/cache.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -7,30 +7,49 @@
 package isabelle
 
 
-import java.util.{Collections, WeakHashMap}
+import java.util.{Collections, WeakHashMap, Map => JMap}
 import java.lang.ref.WeakReference
 
 
-class Cache(initial_size: Int = 131071, max_string: Int = 100)
+object Cache
 {
-  private val table =
-    Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
+  val default_max_string = 100
+  val default_initial_size = 131071
+
+  def make(max_string: Int = default_max_string, initial_size: Int = default_initial_size): Cache =
+    new Cache(max_string, initial_size)
+
+  val none: Cache = make(max_string = 0)
+}
 
-  def size: Int = table.size
+class Cache(max_string: Int, initial_size: Int)
+{
+  val no_cache: Boolean = max_string == 0
 
-  override def toString: String = "Cache(" + size + ")"
+  private val table: JMap[Any, WeakReference[Any]] =
+    if (max_string == 0) null
+    else  Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
+
+  override def toString: String =
+    if (no_cache) "Cache.none" else "Cache(size = " + table.size + ")"
 
   protected def lookup[A](x: A): Option[A] =
   {
-    val ref = table.get(x)
-    if (ref == null) None
-    else Option(ref.asInstanceOf[WeakReference[A]].get)
+    if (table == null) None
+    else {
+      val ref = table.get(x)
+      if (ref == null) None
+      else Option(ref.asInstanceOf[WeakReference[A]].get)
+    }
   }
 
   protected def store[A](x: A): A =
   {
-    table.put(x, new WeakReference[Any](x))
-    x
+    if (table == null) x
+    else {
+      table.put(x, new WeakReference[Any](x))
+      x
+    }
   }
 
   protected def cache_string(x: String): String =
@@ -51,5 +70,6 @@
   }
 
   // main methods
-  def string(x: String): String = synchronized { cache_string(x) }
+  def string(x: String): String =
+    if (no_cache) x else synchronized { cache_string(x) }
 }

--- a/src/Pure/General/properties.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/General/properties.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -37,18 +37,12 @@
 
   def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
 
-  def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T =
-  {
-    val ps = XML.Decode.properties(YXML.parse_body(bs.text))
-    xml_cache match {
-      case None => ps
-      case Some(cache) => cache.props(ps)
-    }
-  }
+  def decode(bs: Bytes, xml_cache: XML.Cache = XML.Cache.none): T =
+    xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
 
   def compress(ps: List[T],
     options: XZ.Options = XZ.options(),
-    cache: XZ.Cache = XZ.cache()): Bytes =
+    cache: XZ.Cache = XZ.Cache()): Bytes =
   {
     if (ps.isEmpty) Bytes.empty
     else {
@@ -58,17 +52,14 @@
   }
 
   def uncompress(bs: Bytes,
-    cache: XZ.Cache = XZ.cache(),
-    xml_cache: Option[XML.Cache] = None): List[T] =
+    cache: XZ.Cache = XZ.Cache(),
+    xml_cache: XML.Cache = XML.Cache.none): List[T] =
   {
     if (bs.is_empty) Nil
     else {
       val ps =
         XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
-      xml_cache match {
-        case None => ps
-        case Some(cache) => ps.map(cache.props)
-      }
+      if (xml_cache.no_cache) ps else ps.map(xml_cache.props)
     }
   }
 

--- a/src/Pure/General/xz.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/General/xz.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -28,7 +28,10 @@
 
   type Cache = ArrayCache
 
-  def no_cache(): ArrayCache = ArrayCache.getDummyCache()
-  def cache(): ArrayCache = ArrayCache.getDefaultCache()
-  def make_cache(): ArrayCache = new BasicArrayCache
+  object Cache
+  {
+    def none: ArrayCache = ArrayCache.getDummyCache()
+    def apply(): ArrayCache = ArrayCache.getDefaultCache()
+    def make(): ArrayCache = new BasicArrayCache
+  }
 }

--- a/src/Pure/PIDE/session.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -127,8 +127,8 @@
 {
   session =>
 
-  val xml_cache: XML.Cache = XML.make_cache()
-  val xz_cache: XZ.Cache = XZ.make_cache()
+  val xml_cache: XML.Cache = XML.Cache.make()
+  val xz_cache: XZ.Cache = XZ.Cache.make()
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
     Command.Blobs_Info.none

--- a/src/Pure/PIDE/xml.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -170,11 +170,18 @@
 
   /** cache **/
 
-  def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
-    new Cache(initial_size, max_string)
+  object Cache
+  {
+    def make(
+        max_string: Int = isabelle.Cache.default_max_string,
+        initial_size: Int = isabelle.Cache.default_initial_size): Cache =
+      new Cache(max_string, initial_size)
 
-  class Cache private[XML](initial_size: Int, max_string: Int)
-    extends isabelle.Cache(initial_size, max_string)
+    val none: Cache = make(max_string = 0)
+  }
+
+  class Cache private[XML](max_string: Int, initial_size: Int)
+    extends isabelle.Cache(max_string, initial_size)
   {
     protected def cache_props(x: Properties.T): Properties.T =
     {
@@ -222,11 +229,16 @@
     }
 
     // main methods
-    def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
-    def markup(x: Markup): Markup = synchronized { cache_markup(x) }
-    def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
-    def body(x: XML.Body): XML.Body = synchronized { cache_body(x) }
-    def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
+    def props(x: Properties.T): Properties.T =
+      if (no_cache) x else synchronized { cache_props(x) }
+    def markup(x: Markup): Markup =
+      if (no_cache) x else synchronized { cache_markup(x) }
+    def tree(x: XML.Tree): XML.Tree =
+      if (no_cache) x else synchronized { cache_tree(x) }
+    def body(x: XML.Body): XML.Body =
+      if (no_cache) x else synchronized { cache_body(x) }
+    def elem(x: XML.Elem): XML.Elem =
+      if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
   }
 
 

--- a/src/Pure/Thy/export.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/Thy/export.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -85,7 +85,7 @@
   def compound_name(a: String, b: String): String = a + ":" + b
 
   def empty_entry(theory_name: String, name: String): Entry =
-    Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.no_cache())
+    Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.Cache.none)
 
   sealed case class Entry(
     session_name: String,

--- a/src/Pure/Thy/export_theory.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -31,7 +31,7 @@
     sessions_structure: Sessions.Structure,
     session_name: String,
     progress: Progress = new Progress,
-    cache: Term.Cache = Term.make_cache()): Session =
+    cache: Term.Cache = Term.Cache.make()): Session =
   {
     val thys =
       sessions_structure.build_requirements(List(session_name)).flatMap(session =>
@@ -42,7 +42,7 @@
             yield {
               progress.echo("Reading theory " + theory)
               read_theory(Export.Provider.database(db, store.xz_cache, session, theory),
-                session, theory, cache = Some(cache))
+                session, theory, cache = cache)
             }
           }
         }))
@@ -107,7 +107,7 @@
   }
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
-    cache: Option[Term.Cache] = None): Theory =
+    cache: Term.Cache = Term.Cache.none): Theory =
   {
     val parents =
       if (theory_name == Thy_Header.PURE) Nil
@@ -134,7 +134,7 @@
         read_typedefs(provider),
         read_datatypes(provider),
         read_spec_rules(provider))
-    if (cache.isDefined) theory.cache(cache.get) else theory
+    if (cache.no_cache) theory else theory.cache(cache)
   }
 
   def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A =
@@ -151,11 +151,11 @@
     })
   }
 
-  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
+  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory =
     read_pure(store, read_theory(_, _, _, cache = cache))
 
   def read_pure_proof(
-      store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
+      store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] =
     read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))
 
 
@@ -375,7 +375,7 @@
   }
 
   def read_proof(
-    provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
+    provider: Export.Provider, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] =
   {
     for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
     yield {
@@ -391,7 +391,7 @@
       val proof = Term_XML.Decode.proof_env(env)(proof_body)
 
       val result = Proof(typargs, args, prop, proof)
-      cache.map(result.cache(_)) getOrElse result
+      if (cache.no_cache) result else result.cache(cache)
     }
   }
 
@@ -400,7 +400,7 @@
     provider: Export.Provider,
     proof: Term.Proof,
     suppress: Thm_Id => Boolean = _ => false,
-    cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] =
+    cache: Term.Cache = Term.Cache.none): List[(Thm_Id, Proof)] =
   {
     var seen = Set.empty[Long]
     var result = SortedMap.empty[Long, (Thm_Id, Proof)]

--- a/src/Pure/Thy/sessions.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -1259,17 +1259,20 @@
     }
   }
 
-  def store(options: Options): Store = new Store(options)
+  def store(options: Options,
+      xml_cache: XML.Cache = XML.Cache.make(),
+      xz_cache: XZ.Cache = XZ.Cache.make()): Store =
+    new Store(options, xml_cache, xz_cache)
 
-  class Store private[Sessions](val options: Options)
+  class Store private[Sessions](
+    val options: Options,
+    val xml_cache: XML.Cache,
+    val xz_cache: XZ.Cache)
   {
     store =>
 
     override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
-    val xml_cache: XML.Cache = XML.make_cache()
-    val xz_cache: XZ.Cache = XZ.make_cache()
-
 
     /* directories */
 
@@ -1405,7 +1408,7 @@
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
       Properties.uncompress(
-        read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache))
+        read_bytes(db, name, column), cache = xz_cache, xml_cache = xml_cache)
 
 
     /* session info */
@@ -1471,7 +1474,7 @@
     }
 
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
-      Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache))
+      Properties.decode(read_bytes(db, name, Session_Info.session_timing), xml_cache = xml_cache)
 
     def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.command_timings)

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