# HG changeset patch
# User wenzelm
# Date 1720033170 -7200
# Node ID d334f158442bf6447df4f971a7c1b120c484fbe2
# Parent  43323d886ea319e63f0eb348018d25ca85cae610
clarified signature: more direct operation;

diff -r 43323d886ea3 -r d334f158442b src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jul 03 20:35:10 2024 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jul 03 20:59:30 2024 +0200
@@ -374,6 +374,9 @@
     }
     else bytes
 
+  def terminated_line: Boolean =
+    size >= 1 && (byte_unchecked(size - 1) == 13 || byte_unchecked(size - 1) == 10)
+
   def trim_line: Bytes =
     if (size >= 2 && byte_unchecked(size - 2) == 13 && byte_unchecked(size - 1) == 10) {
       slice(0, size - 2)
diff -r 43323d886ea3 -r d334f158442b 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))
     }