src/Pure/PIDE/byte_message.scala
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 = {