# HG changeset patch
# User wenzelm
# Date 1666356313 -7200
# Node ID 978f7ca3329fa2505667b1c32d71cd032a1b3132
# Parent  b4daf7577ca0e07673e856225a8b3285350e902d
clarified signature: default cache is actually dummy and not changed dynamically;

diff -r b4daf7577ca0 -r 978f7ca3329f src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Oct 21 13:15:24 2022 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Oct 21 14:45:13 2022 +0200
@@ -616,7 +616,7 @@
       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.none): Option[Bytes] =
     if (errors.isEmpty) None
     else {
       Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
diff -r b4daf7577ca0 -r 978f7ca3329f src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Oct 21 13:15:24 2022 +0200
+++ b/src/Pure/General/bytes.scala	Fri Oct 21 14:45:13 2022 +0200
@@ -193,10 +193,10 @@
 
   /* XZ data compression */
 
-  def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
+  def uncompress(cache: XZ.Cache = XZ.Cache.none): 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.none): Bytes = {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
@@ -204,7 +204,7 @@
 
   def maybe_compress(
     options: XZ.Options = XZ.options(),
-    cache: XZ.Cache = XZ.Cache()
+    cache: XZ.Cache = XZ.Cache.none
   ) : (Boolean, Bytes) = {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
diff -r b4daf7577ca0 -r 978f7ca3329f src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Fri Oct 21 13:15:24 2022 +0200
+++ b/src/Pure/General/properties.scala	Fri Oct 21 14:45:13 2022 +0200
@@ -55,7 +55,7 @@
 
   def compress(ps: List[T],
     options: XZ.Options = XZ.options(),
-    cache: XZ.Cache = XZ.Cache()
+    cache: XZ.Cache = XZ.Cache.none
   ): Bytes = {
     if (ps.isEmpty) Bytes.empty
     else {
diff -r b4daf7577ca0 -r 978f7ca3329f src/Pure/General/xz.scala
--- a/src/Pure/General/xz.scala	Fri Oct 21 13:15:24 2022 +0200
+++ b/src/Pure/General/xz.scala	Fri Oct 21 14:45:13 2022 +0200
@@ -28,7 +28,6 @@
 
   object Cache {
     def none: ArrayCache = ArrayCache.getDummyCache()
-    def apply(): ArrayCache = ArrayCache.getDefaultCache()
     def make(): ArrayCache = new BasicArrayCache
   }