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