clarified signature: default cache is actually dummy and not changed dynamically;
--- 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))).
--- 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)
--- 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 {
--- 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
}