# 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