src/Pure/General/bytes.scala
author wenzelm
Sat, 23 Nov 2019 11:19:18 +0100
changeset 71349 69a22ccd1817
parent 69464 ef051edd4d10
child 71350 f2d848a596d1
permissions -rw-r--r--
tuned;
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
68096
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
    13
import java.util.Base64
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    14
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    15
import org.tukaani.xz.{XZInputStream, XZOutputStream}
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    16
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    17
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    18
object Bytes
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    19
{
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    20
  val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    21
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    22
  def apply(s: CharSequence): Bytes =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    23
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    24
    val str = s.toString
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    25
    if (str.isEmpty) empty
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    26
    else {
62528
aae9a2a855e0 tuned signature;
wenzelm
parents: 60833
diff changeset
    27
      val b = UTF8.bytes(str)
54442
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    28
      new Bytes(b, 0, b.length)
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    29
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    30
  }
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    31
63779
9da65bc75610 more operations;
wenzelm
parents: 62528
diff changeset
    32
  def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
9da65bc75610 more operations;
wenzelm
parents: 62528
diff changeset
    33
54442
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    34
  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
    35
    if (length == 0) empty
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    36
    else {
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    37
      val b = new Array[Byte](length)
55618
995162143ef4 tuned imports;
wenzelm
parents: 54512
diff changeset
    38
      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
    39
      new Bytes(b, 0, b.length)
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    40
    }
c39972ddd672 more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents: 54440
diff changeset
    41
69464
ef051edd4d10 more uniform multi-language operations;
wenzelm
parents: 69458
diff changeset
    42
  val newline: Bytes = apply("\n")
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    43
68111
2277fe496d78 more operations;
wenzelm
parents: 68109
diff changeset
    44
  def base64(s: String): Bytes =
2277fe496d78 more operations;
wenzelm
parents: 68109
diff changeset
    45
  {
2277fe496d78 more operations;
wenzelm
parents: 68109
diff changeset
    46
    val a = Base64.getDecoder.decode(s)
2277fe496d78 more operations;
wenzelm
parents: 68109
diff changeset
    47
    new Bytes(a, 0, a.length)
2277fe496d78 more operations;
wenzelm
parents: 68109
diff changeset
    48
  }
2277fe496d78 more operations;
wenzelm
parents: 68109
diff changeset
    49
68089
dac267cd51fe hexadecimal representation of byte string;
wenzelm
parents: 68018
diff changeset
    50
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    51
  /* read */
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    52
64005
f6e965cf1617 clarified magic values (see also java/io/BufferedInputStream.java);
wenzelm
parents: 64004
diff changeset
    53
  def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    54
    if (limit == 0) empty
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    55
    else {
64005
f6e965cf1617 clarified magic values (see also java/io/BufferedInputStream.java);
wenzelm
parents: 64004
diff changeset
    56
      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
    57
      val buf = new Array[Byte](8192)
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    58
      var m = 0
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    59
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    60
      do {
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    61
        m = stream.read(buf, 0, buf.size min (limit - out.size))
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    62
        if (m != -1) out.write(buf, 0, m)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    63
      } while (m != -1 && limit > out.size)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    64
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
    65
      new Bytes(out.toByteArray, 0, out.size)
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    66
    }
64001
7ecb22be8f03 more general read_stream: return actual byte count;
wenzelm
parents: 63779
diff changeset
    67
7ecb22be8f03 more general read_stream: return actual byte count;
wenzelm
parents: 63779
diff changeset
    68
  def read(file: JFile): Bytes =
71349
wenzelm
parents: 69464
diff changeset
    69
    using(new FileInputStream(file))(read_stream(_, limit = file.length.toInt))
64229
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    70
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    71
  def read(path: Path): Bytes = read(path.file)
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    72
65070
1222c010bff7 more operations;
wenzelm
parents: 64370
diff changeset
    73
  def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
1222c010bff7 more operations;
wenzelm
parents: 64370
diff changeset
    74
64229
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    75
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    76
  /* write */
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    77
69403
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69375
diff changeset
    78
  def write(file: JFile, bytes: Bytes): Unit =
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69375
diff changeset
    79
    using(new FileOutputStream(file))(bytes.write_stream(_))
64229
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    80
12aa3980f65c more operations;
wenzelm
parents: 64224
diff changeset
    81
  def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    82
}
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    83
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    84
final class Bytes private(
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    85
  protected val bytes: Array[Byte],
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    86
  protected val offset: Int,
60833
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
    87
  val length: Int) extends CharSequence
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    88
{
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    89
  /* equality */
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    90
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    91
  override def equals(that: Any): Boolean =
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    92
  {
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    93
    that match {
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    94
      case other: Bytes =>
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    95
        if (this eq other) true
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    96
        else if (length != other.length) false
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    97
        else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    98
      case _ => false
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
    99
    }
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   100
  }
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   101
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   102
  private lazy val hash: Int =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   103
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   104
    var h = 0
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   105
    for (i <- offset until offset + length) {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   106
      val b = bytes(i).asInstanceOf[Int] & 0xFF
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   107
      h = 31 * h + b
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   108
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   109
    h
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   110
  }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   111
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   112
  override def hashCode(): Int = hash
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   113
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   114
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   115
  /* content */
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   116
54512
7a92ed889da4 persistent value;
wenzelm
parents: 54444
diff changeset
   117
  lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   118
69458
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   119
  def is_empty: Boolean = length == 0
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   120
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   121
  def iterator: Iterator[Byte] =
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   122
    for (i <- (offset until (offset + length)).iterator)
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   123
      yield bytes(i)
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   124
69375
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   125
  def array: Array[Byte] =
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   126
  {
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   127
    val a = new Array[Byte](length)
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   128
    System.arraycopy(bytes, offset, a, 0, length)
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   129
    a
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   130
  }
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 68167
diff changeset
   131
65279
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   132
  def text: String =
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   133
    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
fa62e095d8f1 clarified signature (again, see also 3ed43cfc8b14);
wenzelm
parents: 65070
diff changeset
   134
68096
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   135
  def base64: String =
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   136
  {
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   137
    val b =
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   138
      if (offset == 0 && length == bytes.length) bytes
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   139
      else Bytes(bytes, offset, length).bytes
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   140
    Base64.getEncoder.encodeToString(b)
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   141
  }
0b66aca9c965 more operations;
wenzelm
parents: 68089
diff changeset
   142
68109
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 68096
diff changeset
   143
  def maybe_base64: (Boolean, String) =
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 68096
diff changeset
   144
  {
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 68096
diff changeset
   145
    val s = text
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 68096
diff changeset
   146
    if (this == Bytes(s)) (false, s) else (true, base64)
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 68096
diff changeset
   147
  }
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 68096
diff changeset
   148
68150
f0f34cbed539 clarified output: avoid costly operations on huge blobs;
wenzelm
parents: 68149
diff changeset
   149
  override def toString: String = "Bytes(" + length + ")"
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   150
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   151
  def isEmpty: Boolean = length == 0
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   152
65630
c41bbf657310 more operations;
wenzelm
parents: 65279
diff changeset
   153
  def proper: Option[Bytes] = if (isEmpty) None else Some(this)
c41bbf657310 more operations;
wenzelm
parents: 65279
diff changeset
   154
  def proper_text: Option[String] = if (isEmpty) None else Some(text)
c41bbf657310 more operations;
wenzelm
parents: 65279
diff changeset
   155
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   156
  def +(other: Bytes): Bytes =
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   157
    if (other.isEmpty) this
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   158
    else if (isEmpty) other
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   159
    else {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   160
      val new_bytes = new Array[Byte](length + other.length)
55618
995162143ef4 tuned imports;
wenzelm
parents: 54512
diff changeset
   161
      System.arraycopy(bytes, offset, new_bytes, 0, length)
995162143ef4 tuned imports;
wenzelm
parents: 54512
diff changeset
   162
      System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   163
      new Bytes(new_bytes, 0, new_bytes.length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   164
    }
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   165
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   166
60833
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   167
  /* CharSequence operations */
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   168
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   169
  def charAt(i: Int): Char =
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   170
    if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   171
    else throw new IndexOutOfBoundsException
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   172
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   173
  def subSequence(i: Int, j: Int): Bytes =
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   174
  {
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   175
    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
   176
    else throw new IndexOutOfBoundsException
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   177
  }
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   178
69458
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   179
  def trim_line: Bytes =
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   180
    if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   181
      subSequence(0, length - 2)
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   182
    else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   183
      subSequence(0, length - 1)
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   184
    else this
51e696887b81 more uniform multi-language operations;
wenzelm
parents: 69403
diff changeset
   185
60833
d201996f72a8 provide CharSequence operations as well;
wenzelm
parents: 55618
diff changeset
   186
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   187
  /* streams */
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   188
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   189
  def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   190
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   191
  def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   192
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   193
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   194
  /* XZ data compression */
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 54439
diff changeset
   195
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   196
  def uncompress(cache: XZ.Cache = XZ.cache()): Bytes =
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   197
    using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   198
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   199
  def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes =
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   200
  {
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   201
    val result = new ByteArrayOutputStream(length)
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67805
diff changeset
   202
    using(new XZOutputStream(result, options, cache))(write_stream(_))
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   203
    new Bytes(result.toByteArray, 0, result.size)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64001
diff changeset
   204
  }
68167
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   205
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   206
  def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache())
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   207
    : (Boolean, Bytes) =
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   208
  {
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   209
    val compressed = compress(options = options, cache = cache)
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   210
    if (compressed.length < length) (true, compressed) else (false, this)
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68150
diff changeset
   211
  }
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
   212
}