--- a/src/Pure/General/bytes.scala Thu Nov 14 17:39:32 2013 +0100
+++ b/src/Pure/General/bytes.scala Fri Nov 15 19:31:10 2013 +0100
@@ -20,11 +20,19 @@
val str = s.toString
if (str.isEmpty) empty
else {
- val bytes = str.getBytes(UTF8.charset)
- new Bytes(bytes, 0, bytes.length)
+ val b = str.getBytes(UTF8.charset)
+ new Bytes(b, 0, b.length)
}
}
+ def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
+ if (length == 0) empty
+ else {
+ val b = new Array[Byte](length)
+ java.lang.System.arraycopy(a, offset, b, 0, length)
+ new Bytes(b, 0, b.length)
+ }
+
/* read */