src/Pure/General/bytes.scala
author wenzelm
Sat, 05 May 2018 21:44:18 +0200
changeset 68087 dac267cd51fe
parent 68018 3747fe57eb67
child 68094 0b66aca9c965
permissions -rw-r--r--
hexadecimal representation of byte string;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/bytes.scala
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     3
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     4
Immutable byte vectors versus UTF8 strings.
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     5
*/
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     6
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     7
package isabelle
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     8
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     9
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    10
import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
64229
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    11
  OutputStream, InputStream, FileInputStream, FileOutputStream}
65070
1222c010bff7 more operations;
wenzelm
parents: 64370
diff changeset
    12
import java.net.URL
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    13
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    14
import org.tukaani.xz.{XZInputStream, XZOutputStream}
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    15
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    16
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    17
object Bytes
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    18
{
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    19
  val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    20
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    21
  def apply(s: CharSequence): Bytes =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    22
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    23
    val str = s.toString
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    24
    if (str.isEmpty) empty
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    25
    else {
62527
aae9a2a855e0 tuned signature;
wenzelm
parents: 60833
diff changeset
    26
      val b = UTF8.bytes(str)
54442
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    27
      new Bytes(b, 0, b.length)
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    28
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    29
  }
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    30
63779
9da65bc75610 more operations;
wenzelm
parents: 62527
diff changeset
    31
  def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
9da65bc75610 more operations;
wenzelm
parents: 62527
diff changeset
    32
54442
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    33
  def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    34
    if (length == 0) empty
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    35
    else {
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    36
      val b = new Array[Byte](length)
55618
995162143ef4 tuned imports;
wenzelm
parents: 54512
diff changeset
    37
      System.arraycopy(a, offset, b, 0, length)
54442
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    38
      new Bytes(b, 0, b.length)
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    39
    }
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    40
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    41
68087
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    42
  def hex(s: String): Bytes =
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    43
  {
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    44
    def err(): Nothing = error("Malformed hexadecimal representation of bytes\n" + s)
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    45
    val len = s.length
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    46
    if (len % 2 != 0) err()
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    47
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    48
    val n = len / 2
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    49
    val a = new Array[Byte](n)
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    50
    for (i <- 0 until n) {
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    51
      val j = 2 * i
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    52
      try { a(i) = Integer.parseInt(s.substring(j, j + 2), 16).toByte }
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    53
      catch { case _: NumberFormatException => err() }
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    54
    }
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    55
    new Bytes(a, 0, n)
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    56
  }
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    57
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    58
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    59
  /* read */
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    60
64005
f6e965cf1617 clarified magic values (see also java/io/BufferedInputStream.java);
wenzelm
parents: 64004
diff changeset
    61
  def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    62
    if (limit == 0) empty
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    63
    else {
64005
f6e965cf1617 clarified magic values (see also java/io/BufferedInputStream.java);
wenzelm
parents: 64004
diff changeset
    64
      val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) hint else limit)
f6e965cf1617 clarified magic values (see also java/io/BufferedInputStream.java);
wenzelm
parents: 64004
diff changeset
    65
      val buf = new Array[Byte](8192)
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    66
      var m = 0
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    67
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    68
      do {
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    69
        m = stream.read(buf, 0, buf.size min (limit - out.size))
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    70
        if (m != -1) out.write(buf, 0, m)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    71
      } while (m != -1 && limit > out.size)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    72
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    73
      new Bytes(out.toByteArray, 0, out.size)
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    74
    }
64001
7ecb22be8f03 more general read_stream: return actual byte count;
wenzelm
parents: 63779
diff changeset
    75
67805
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    76
  def read_block(stream: InputStream, length: Int): Option[Bytes] =
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    77
  {
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    78
    val bytes = read_stream(stream, limit = length)
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    79
    if (bytes.length == length) Some(bytes) else None
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    80
  }
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    81
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    82
  def read_line(stream: InputStream): Option[Bytes] =
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    83
  {
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    84
    val out = new ByteArrayOutputStream(100)
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    85
    var c = 0
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    86
    while ({ c = stream.read; c != -1 && c != 10 }) out.write(c)
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    87
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    88
    if (c == -1 && out.size == 0) None
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    89
    else {
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    90
      val a = out.toByteArray
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    91
      val n = a.length
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    92
      val b = if (n > 0 && a(n - 1) == 13) a.take(n - 1) else a
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    93
      Some(new Bytes(b, 0, b.length))
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    94
    }
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    95
  }
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 65630
diff changeset
    96
64001
7ecb22be8f03 more general read_stream: return actual byte count;
wenzelm
parents: 63779
diff changeset
    97
  def read(file: JFile): Bytes =
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    98
    using(new FileInputStream(file))(read_stream(_, file.length.toInt))
64229
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    99
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   100
  def read(path: Path): Bytes = read(path.file)
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   101
65070
1222c010bff7 more operations;
wenzelm
parents: 64370
diff changeset
   102
  def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
1222c010bff7 more operations;
wenzelm
parents: 64370
diff changeset
   103
64229
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   104
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   105
  /* write */
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   106
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   107
  def write(file: JFile, bytes: Bytes)
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   108
  {
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   109
    val stream = new FileOutputStream(file)
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   110
    try { bytes.write_stream(stream) } finally { stream.close }
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   111
  }
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   112
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
   113
  def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   114
}
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   115
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   116
final class Bytes private(
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   117
  protected val bytes: Array[Byte],
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   118
  protected val offset: Int,
60833
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   119
  val length: Int) extends CharSequence
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   120
{
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   121
  /* equality */
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   122
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   123
  override def equals(that: Any): Boolean =
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   124
  {
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   125
    that match {
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   126
      case other: Bytes =>
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   127
        if (this eq other) true
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   128
        else if (length != other.length) false
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   129
        else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   130
      case _ => false
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   131
    }
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   132
  }
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   133
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   134
  private lazy val hash: Int =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   135
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   136
    var h = 0
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   137
    for (i <- offset until offset + length) {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   138
      val b = bytes(i).asInstanceOf[Int] & 0xFF
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   139
      h = 31 * h + b
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   140
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   141
    h
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   142
  }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   143
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   144
  override def hashCode(): Int = hash
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   145
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   146
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   147
  /* content */
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   148
54512
7a92ed889da4 persistent value;
wenzelm
parents: 54444
diff changeset
   149
  lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   150
65279
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   151
  def text: String =
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   152
    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   153
54444
a2290f36d1d6 prefer UTF8.decode_permissive;
wenzelm
parents: 54442
diff changeset
   154
  override def toString: String =
64224
3ed43cfc8b14 clarified treatment of non-text bytes;
wenzelm
parents: 64005
diff changeset
   155
  {
65279
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   156
    val str = text
64224
3ed43cfc8b14 clarified treatment of non-text bytes;
wenzelm
parents: 64005
diff changeset
   157
    if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
3ed43cfc8b14 clarified treatment of non-text bytes;
wenzelm
parents: 64005
diff changeset
   158
  }
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   159
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   160
  def isEmpty: Boolean = length == 0
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   161
65630
c41bbf657310 more operations;
wenzelm
parents: 65279
diff changeset
   162
  def proper: Option[Bytes] = if (isEmpty) None else Some(this)
c41bbf657310 more operations;
wenzelm
parents: 65279
diff changeset
   163
  def proper_text: Option[String] = if (isEmpty) None else Some(text)
c41bbf657310 more operations;
wenzelm
parents: 65279
diff changeset
   164
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   165
  def +(other: Bytes): Bytes =
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   166
    if (other.isEmpty) this
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   167
    else if (isEmpty) other
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   168
    else {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   169
      val new_bytes = new Array[Byte](length + other.length)
55618
995162143ef4 tuned imports;
wenzelm
parents: 54512
diff changeset
   170
      System.arraycopy(bytes, offset, new_bytes, 0, length)
995162143ef4 tuned imports;
wenzelm
parents: 54512
diff changeset
   171
      System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   172
      new Bytes(new_bytes, 0, new_bytes.length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   173
    }
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   174
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   175
60833
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   176
  /* CharSequence operations */
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   177
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   178
  def charAt(i: Int): Char =
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   179
    if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   180
    else throw new IndexOutOfBoundsException
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   181
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   182
  def subSequence(i: Int, j: Int): Bytes =
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   183
  {
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   184
    if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   185
    else throw new IndexOutOfBoundsException
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   186
  }
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   187
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   188
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   189
  /* streams */
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   190
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   191
  def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   192
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   193
  def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   194
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   195
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   196
  /* XZ data compression */
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   197
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   198
  def uncompress(cache: XZ.Cache = XZ.cache()): Bytes =
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   199
    using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   200
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   201
  def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes =
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   202
  {
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   203
    val result = new ByteArrayOutputStream(length)
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   204
    using(new XZOutputStream(result, options, cache))(write_stream(_))
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   205
    new Bytes(result.toByteArray, 0, result.size)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   206
  }
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   207
}