clarified signature: discontinue somewhat misleading Bytes <: CharSequence;

--- a/src/Pure/General/bytes.scala	Tue Jun 11 16:02:33 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jun 11 16:32:10 2024 +0200
@@ -132,7 +132,7 @@
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
-  val length: Int) extends Bytes.Vec with CharSequence {
+  val length: Int) extends Bytes.Vec {
   /* equality */
 
   override def equals(that: Any): Boolean = {
@@ -224,21 +224,18 @@
     else throw new IndexOutOfBoundsException
 
 
-  /* CharSequence operations */
-
-  def charAt(i: Int): Char = apply(i).asInstanceOf[Char]
+  /* slice */
 
-  def subSequence(i: Int, j: Int): Bytes = {
-    if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
+  def slice(i: Long, j: Long): Bytes =
+    if (0 <= i && i <= j && j <= size) new Bytes(bytes, (offset + i).toInt, (j - i).toInt)
     else throw new IndexOutOfBoundsException
-  }
 
   def trim_line: Bytes =
-    if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) {
-      subSequence(0, length - 2)
+    if (size >= 2 && apply(size - 2) == 13 && apply(size - 1) == 10) {
+      slice(0, size - 2)
     }
-    else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) {
-      subSequence(0, length - 1)
+    else if (size >= 1 && (apply(size - 1) == 13 || apply(size - 1) == 10)) {
+      slice(0, size - 1)
     }
     else this
 

--- a/src/Pure/PIDE/byte_message.scala	Tue Jun 11 16:02:33 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Tue Jun 11 16:32:10 2024 +0200
@@ -81,10 +81,13 @@
   private def is_length(msg: Bytes): Boolean =
     !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
 
-  private def is_terminated(msg: Bytes): Boolean = {
-    val len = msg.length
-    len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
-  }
+  private def is_terminated(msg: Bytes): Boolean =
+    msg.size match {
+      case size if size > 0 =>
+        val c = msg(size - 1)
+        c <= Char.MaxValue && Symbol.is_ascii_line_terminator(c.toChar)
+      case _ => false
+    }
 
   def write_line_message(stream: OutputStream, msg: Bytes): Unit = {
     if (is_length(msg) || is_terminated(msg))

--- a/src/Pure/System/web_app.scala	Tue Jun 11 16:02:33 2024 +0200
+++ b/src/Pure/System/web_app.scala	Tue Jun 11 16:32:10 2024 +0200
@@ -120,12 +120,12 @@
 
             // text might be shorter than bytes because of misinterpreted characters
             var found = false
-            var bytes_i = 0
-            while (!found && bytes_i < bytes.length) {
+            var bytes_i = 0L
+            while (!found && bytes_i < bytes.size) {
               var sep_ok = true
               var sep_i = 0
               while (sep_ok && sep_i < sep.length) {
-                if (bytes.charAt(bytes_i + sep_i) == sep.charAt(sep_i)) {
+                if (bytes(bytes_i + sep_i) == sep(sep_i)) {
                   sep_i += 1
                 } else {
                   bytes_i += 1
@@ -135,8 +135,8 @@
               if (sep_ok) found = true
             }
 
-            val before_bytes = bytes.subSequence(0, bytes_i)
-            val after_bytes = bytes.subSequence(bytes_i + sep.length, bytes.length)
+            val before_bytes = bytes.slice(0, bytes_i)
+            val after_bytes = bytes.slice(bytes_i + sep.length, bytes.size)
 
             Some(Seq(before_text, before_bytes), Seq(after_text, after_bytes))
           } else None
@@ -147,7 +147,7 @@
 
       def perhaps_unprefix(pfx: String, s: Seq): Seq =
         Library.try_unprefix(pfx, s.text) match {
-          case Some(text) => Seq(text, s.bytes.subSequence(pfx.length, s.bytes.length))
+          case Some(text) => Seq(text, s.bytes.slice(pfx.length, s.bytes.size))
           case None => s
         }