src/Pure/General/bytes.scala
changeset 54442 c39972ddd672
parent 54440 2c4940d2edf7
child 54444 a2290f36d1d6
--- 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 */