--- 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(
--- 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()
--- 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))
--- 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 =
{
--- 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 =