src/Pure/PIDE/byte_message.scala

--- a/src/Pure/PIDE/byte_message.scala	Wed Jul 03 20:35:10 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Wed Jul 03 20:59:30 2024 +0200
@@ -85,16 +85,8 @@
     !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) &&
       Value.Long.unapply(msg.text).isDefined
 
-  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)) {
+    if (is_length(msg) || msg.terminated_line) {
       error ("Bad content for line message:\n" ++ msg.text.take(100))
     }