changeset 80548 | d1662f1296db |
parent 80493 | d334f158442b |
child 80549 | 769a52499f12 |
--- a/src/Pure/PIDE/byte_message.scala Mon Jul 08 22:28:02 2024 +0100 +++ b/src/Pure/PIDE/byte_message.scala Tue Jul 09 12:32:33 2024 +0200 @@ -82,7 +82,7 @@ Value.Long.unapply(str).isDefined private def is_length(msg: Bytes): Boolean = - !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) && + !msg.is_empty && msg.byte_iterator.forall(Symbol.is_ascii_digit) && Value.Long.unapply(msg.text).isDefined def write_line_message(stream: OutputStream, msg: Bytes): Unit = {