# HG changeset patch
# User wenzelm
# Date 1438248778 -7200
# Node ID d201996f72a89a4c396ccd788c84d53100797286
# Parent  1cdc63224ed3fa5b0e15d04afaa49deba534657e
provide CharSequence operations as well;

diff -r 1cdc63224ed3 -r d201996f72a8 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jul 29 15:52:57 2015 +0200
+++ b/src/Pure/General/bytes.scala	Thu Jul 30 11:32:58 2015 +0200
@@ -59,7 +59,7 @@
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
-  val length: Int)
+  val length: Int) extends CharSequence
 {
   /* equality */
 
@@ -107,6 +107,19 @@
     }
 
 
+  /* CharSequence operations */
+
+  def charAt(i: Int): Char =
+    if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+    else throw new IndexOutOfBoundsException
+
+  def subSequence(i: Int, j: Int): Bytes =
+  {
+    if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
+    else throw new IndexOutOfBoundsException
+  }
+
+
   /* write */
 
   def write(stream: OutputStream): Unit = stream.write(bytes, offset, length)