--- a/src/Pure/General/bytes.scala Sun May 13 16:05:29 2018 +0200
+++ b/src/Pure/General/bytes.scala Sun May 13 16:26:01 2018 +0200
@@ -205,4 +205,11 @@
using(new XZOutputStream(result, options, cache))(write_stream(_))
new Bytes(result.toByteArray, 0, result.size)
}
+
+ def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache())
+ : (Boolean, Bytes) =
+ {
+ val compressed = compress(options = options, cache = cache)
+ if (compressed.length < length) (true, compressed) else (false, this)
+ }
}