# HG changeset patch
# User wenzelm
# Date 1526222256 -7200
# Node ID 395432e7516e5a6f51cc77ee95ef9296b7e12a25
# Parent  a9b49430f0614b9225a9b2a929c5226d665da463
tuned signature;

diff -r a9b49430f061 -r 395432e7516e src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/Admin/build_log.scala	Sun May 13 16:37:36 2018 +0200
@@ -253,7 +253,7 @@
 
     /* properties (YXML) */
 
-    val xml_cache = new XML.Cache()
+    val xml_cache = XML.make_cache()
 
     def parse_props(text: String): Properties.T =
       try {
@@ -881,7 +881,7 @@
 
   class Store private[Build_Log](options: Options)
   {
-    val xml_cache: XML.Cache = new XML.Cache()
+    val xml_cache: XML.Cache = XML.make_cache()
     val xz_cache: XZ.Cache = XZ.make_cache()
 
     def open_database(
diff -r a9b49430f061 -r 395432e7516e src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Sun May 13 16:37:36 2018 +0200
@@ -118,7 +118,7 @@
 {
   session =>
 
-  val xml_cache: XML.Cache = new XML.Cache()
+  val xml_cache: XML.Cache = XML.make_cache()
   val xz_cache: XZ.Cache = XZ.make_cache()
 
 
diff -r a9b49430f061 -r 395432e7516e src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/PIDE/xml.scala	Sun May 13 16:37:36 2018 +0200
@@ -154,7 +154,10 @@
 
   /** cache for partial sharing (weak table) **/
 
-  class Cache(initial_size: Int = 131071, max_string: Int = 100)
+  def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
+    new Cache(initial_size, max_string)
+
+  class Cache private[XML](initial_size: Int, max_string: Int)
   {
     private val table =
       Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
diff -r a9b49430f061 -r 395432e7516e src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun May 13 16:37:36 2018 +0200
@@ -42,7 +42,7 @@
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
-    xml_cache: XML.Cache = new XML.Cache(),
+    xml_cache: XML.Cache = XML.make_cache(),
     sessions: Option[Sessions.Structure] = None,
     store: Sessions.Store = Sessions.store()): Prover =
   {
diff -r a9b49430f061 -r 395432e7516e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun May 13 16:37:36 2018 +0200
@@ -973,7 +973,7 @@
 
     /* SQL database content */
 
-    val xml_cache = new XML.Cache()
+    val xml_cache = XML.make_cache()
     val xz_cache = XZ.make_cache()
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =