# HG changeset patch
# User wenzelm
# Date 1524255462 -7200
# Node ID 3747fe57eb6799f84cf5692bbe0bc74a6b7afb0e
# Parent  5eb4081e6bf6cea52e03467b8b94b37f9a5c18b9
support for XZ.Cache;

diff -r 5eb4081e6bf6 -r 3747fe57eb67 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Apr 20 22:17:42 2018 +0200
@@ -675,13 +675,18 @@
       errors = log_file.filter_lines(ERROR_MESSAGE_MARKER).map(Library.decode_lines(_)))
   }
 
-  def compress_errors(errors: List[String]): 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())
+    else {
+      Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
+        compress(cache = cache))
+    }
 
-  def uncompress_errors(bytes: Bytes): List[String] =
+  def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] =
     if (bytes.isEmpty) Nil
-    else XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress().text))
+    else {
+      XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress(cache = cache).text))
+    }
 
 
 
@@ -877,6 +882,7 @@
   class Store private[Build_Log](options: Options)
   {
     val xml_cache: XML.Cache = new XML.Cache()
+    val xz_cache: XZ.Cache = XZ.make_cache()
 
     def open_database(
       user: String = options.string("build_log_database_user"),
@@ -1011,7 +1017,7 @@
           stmt.double(13) = session.ml_timing.factor
           stmt.long(14) = session.heap_size
           stmt.string(15) = session.status.map(_.toString)
-          stmt.bytes(16) = compress_errors(session.errors)
+          stmt.bytes(16) = compress_errors(session.errors, cache = xz_cache)
           stmt.string(17) = session.sources
           stmt.execute()
         }
@@ -1049,7 +1055,7 @@
       {
         val ml_stats: List[(String, Option[Bytes])] =
           Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
-            { case (a, b) => (a, Properties.compress(b.ml_statistics).proper) },
+            { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) },
             build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
         val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
         for ((session_name, ml_statistics) <- entries) {
@@ -1178,10 +1184,12 @@
                 sources = res.get_string(Data.sources),
                 heap_size = res.get_long(Data.heap_size),
                 status = res.get_string(Data.status).map(Session_Status.withName(_)),
-                errors = uncompress_errors(res.bytes(Data.errors)),
+                errors = uncompress_errors(res.bytes(Data.errors), cache = xz_cache),
                 ml_statistics =
-                  if (ml_statistics)
-                    Properties.uncompress(res.bytes(Data.ml_statistics), Some(xml_cache))
+                  if (ml_statistics) {
+                    Properties.uncompress(
+                      res.bytes(Data.ml_statistics), cache = xz_cache, Some(xml_cache))
+                  }
                   else Nil)
             session_name -> session_entry
           }).toMap
diff -r 5eb4081e6bf6 -r 3747fe57eb67 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/Pure/Admin/build_status.scala	Fri Apr 20 22:17:42 2018 +0200
@@ -204,6 +204,7 @@
       data_hosts.getOrElse(data_name, Set.empty)
 
     val store = Build_Log.store(options)
+
     using(store.open_database())(db =>
     {
       for (profile <- profiles.sortBy(_.description)) {
@@ -272,8 +273,10 @@
 
             val ml_stats =
               ML_Statistics(
-                if (ml_statistics)
-                  Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
+                if (ml_statistics) {
+                  Properties.uncompress(
+                    res.bytes(Build_Log.Data.ml_statistics), cache = store.xz_cache)
+                }
                 else Nil,
                 domain = ml_statistics_domain,
                 heading = session_name + print_version(isabelle_version, afp_version, chapter))
@@ -300,7 +303,9 @@
                 average_heap = ml_stats.average_heap_size,
                 stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
-                errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors)))
+                errors =
+                  Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors),
+                    cache = store.xz_cache))
 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
             val session =
diff -r 5eb4081e6bf6 -r 3747fe57eb67 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/Pure/General/bytes.scala	Fri Apr 20 22:17:42 2018 +0200
@@ -178,13 +178,13 @@
 
   /* XZ data compression */
 
-  def uncompress(): Bytes =
-    using(new XZInputStream(stream()))(Bytes.read_stream(_, hint = length))
+  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()): Bytes =
+  def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes =
   {
     val result = new ByteArrayOutputStream(length)
-    using(new XZOutputStream(result, options))(write_stream(_))
+    using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 }
diff -r 5eb4081e6bf6 -r 3747fe57eb67 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/Pure/General/properties.scala	Fri Apr 20 22:17:42 2018 +0200
@@ -46,17 +46,25 @@
     }
   }
 
-  def compress(ps: List[T], options: XZ.Options = XZ.options()): Bytes =
+  def compress(ps: List[T],
+    options: XZ.Options = XZ.options(),
+    cache: XZ.Cache = XZ.cache()): Bytes =
   {
     if (ps.isEmpty) Bytes.empty
-    else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
+    else {
+      Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
+        compress(options = options, cache = cache)
+    }
   }
 
-  def uncompress(bs: Bytes, xml_cache: Option[XML.Cache] = None): List[T] =
+  def uncompress(bs: Bytes,
+    cache: XZ.Cache = XZ.cache(),
+    xml_cache: Option[XML.Cache] = None): List[T] =
   {
     if (bs.isEmpty) Nil
     else {
-      val ps = XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text))
+      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(_))
diff -r 5eb4081e6bf6 -r 3747fe57eb67 src/Pure/General/xz.scala
--- a/src/Pure/General/xz.scala	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/Pure/General/xz.scala	Fri Apr 20 22:17:42 2018 +0200
@@ -7,11 +7,13 @@
 package isabelle
 
 
-import org.tukaani.xz.LZMA2Options
+import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache}
 
 
 object XZ
 {
+  /* options */
+
   type Options = LZMA2Options
 
   def options(preset: Int = 3): Options =
@@ -20,4 +22,12 @@
     opts.setPreset(preset)
     opts
   }
+
+
+  /* cache */
+
+  type Cache = ArrayCache
+
+  def cache(): ArrayCache = ArrayCache.getDefaultCache()
+  def make_cache(): ArrayCache = new BasicArrayCache
 }
diff -r 5eb4081e6bf6 -r 3747fe57eb67 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 20 22:17:42 2018 +0200
@@ -974,6 +974,7 @@
     /* SQL database content */
 
     val xml_cache = new XML.Cache()
+    val xz_cache = XZ.make_cache()
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
@@ -984,7 +985,8 @@
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
-      Properties.uncompress(read_bytes(db, name, column), Some(xml_cache))
+      Properties.uncompress(
+        read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache))
 
 
     /* output */
@@ -1040,11 +1042,11 @@
         {
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
-          stmt.bytes(3) = Properties.compress(build_log.command_timings)
-          stmt.bytes(4) = Properties.compress(build_log.theory_timings)
-          stmt.bytes(5) = Properties.compress(build_log.ml_statistics)
-          stmt.bytes(6) = Properties.compress(build_log.task_statistics)
-          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors)
+          stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
+          stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
+          stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
+          stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
+          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache)
           stmt.string(8) = build.sources
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
@@ -1070,7 +1072,7 @@
       read_properties(db, name, Session_Info.task_statistics)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
-      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors))
+      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache)
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {