src/Pure/Admin/build_log.scala

       yield entry
 
 
     /* 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))) }
       catch { case _: XML.Error => log_file.err("malformed properties") }
 

       task_statistics =
         if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil,
       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))
     }
 

   }
 
 
   /* database access */
 
-  def store(options: Options): Store = new Store(options)
-
-  class Store private[Build_Log](options: Options)
-  {
-    val xml_cache: XML.Cache = XML.make_cache()
-    val xz_cache: XZ.Cache = XZ.make_cache()
-
+  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,
+    val xml_cache: XML.Cache,
+    val xz_cache: XZ.Cache)
+  {
     def open_database(
       user: String = options.string("build_log_database_user"),
       password: String = options.string("build_log_database_password"),
       database: String = options.string("build_log_database_name"),
       host: String = options.string("build_log_database_host"),

                 status = res.get_string(Data.status).map(Session_Status.withName),
                 errors = uncompress_errors(res.bytes(Data.errors), cache = xz_cache),
                 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
           }).toMap
         })