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