src/Pure/PIDE/byte_message.scala

--- 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))