# HG changeset patch
# User wenzelm
# Date 1384444532 -3600
# Node ID 621a155c77150043f876b791aebc0cb5821416d2
# Parent  6ccc6130140ccbb8bd71b5e77c5db17d785ff606
immutable byte vectors versus UTF8 strings;

diff -r 6ccc6130140c -r 621a155c7715 src/Pure/General/bytes.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/bytes.scala	Thu Nov 14 16:55:32 2013 +0100
@@ -0,0 +1,73 @@
+/*  Title:      Pure/General/bytes.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Immutable byte vectors versus UTF8 strings.
+*/
+
+package isabelle
+
+
+object Bytes
+{
+  val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
+
+  def apply(s: CharSequence): Bytes =
+  {
+    val str = s.toString
+    if (str.isEmpty) empty
+    else {
+      val bytes = UTF8.string_bytes(str)
+      new Bytes(bytes, 0, bytes.length)
+    }
+  }
+}
+
+final class Bytes private(
+  protected val bytes: Array[Byte],
+  protected val offset: Int,
+  val length: Int)
+{
+  /* equality */
+
+  private lazy val hash: Int =
+  {
+    var h = 0
+    for (i <- offset until offset + length) {
+      val b = bytes(i).asInstanceOf[Int] & 0xFF
+      h = 31 * h + b
+    }
+    h
+  }
+
+  override def hashCode(): Int = hash
+
+  override def equals(that: Any): Boolean =
+  {
+    that match {
+      case other: Bytes =>
+        if (this eq other) true
+        else if (length != other.length) false
+        else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
+      case _ => false
+    }
+  }
+
+
+  /* content */
+
+  override def toString: String = new String(bytes, offset, length, UTF8.charset)
+
+  def is_empty: Boolean = length == 0
+
+  def +(other: Bytes): Bytes =
+    if (other.is_empty) this
+    else if (is_empty) other
+    else {
+      val new_bytes = new Array[Byte](length + other.length)
+      java.lang.System.arraycopy(bytes, offset, new_bytes, 0, length)
+      java.lang.System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
+      new Bytes(new_bytes, 0, new_bytes.length)
+    }
+}
+
diff -r 6ccc6130140c -r 621a155c7715 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Nov 14 10:59:22 2013 +0100
+++ b/src/Pure/build-jars	Thu Nov 14 16:55:32 2013 +0100
@@ -13,6 +13,7 @@
   Concurrent/future.scala
   Concurrent/simple_thread.scala
   Concurrent/volatile.scala
+  General/bytes.scala
   General/exn.scala
   General/file.scala
   General/graph.scala