src/Pure/General/bytes.scala
changeset 68167 327bb0f5f768
parent 68150 f0f34cbed539
child 69365 c5b3860d29ef
     1.1 --- a/src/Pure/General/bytes.scala	Sun May 13 16:05:29 2018 +0200
     1.2 +++ b/src/Pure/General/bytes.scala	Sun May 13 16:26:01 2018 +0200
     1.3 @@ -205,4 +205,11 @@
     1.4      using(new XZOutputStream(result, options, cache))(write_stream(_))
     1.5      new Bytes(result.toByteArray, 0, result.size)
     1.6    }
     1.7 +
     1.8 +  def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache())
     1.9 +    : (Boolean, Bytes) =
    1.10 +  {
    1.11 +    val compressed = compress(options = options, cache = cache)
    1.12 +    if (compressed.length < length) (true, compressed) else (false, this)
    1.13 +  }
    1.14  }