# HG changeset patch
# User wenzelm
# Date 1720521153 -7200
# Node ID d1662f1296dbcc583eb15139bb6ca9a20e6b84f5
# Parent  e066cc867115b9c3a156e029c766b4d05011ef68
tuned signature;

diff -r e066cc867115 -r d1662f1296db src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Jul 08 22:28:02 2024 +0100
+++ b/src/Pure/General/symbol.scala	Tue Jul 09 12:32:33 2024 +0200
@@ -51,6 +51,7 @@
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
 
   def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
+  def is_ascii_digit(b: Byte): Boolean = is_ascii_digit(b.toChar)
 
   def is_ascii_hex(c: Char): Boolean =
     '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
diff -r e066cc867115 -r d1662f1296db src/Pure/General/value.scala
--- a/src/Pure/General/value.scala	Mon Jul 08 22:28:02 2024 +0100
+++ b/src/Pure/General/value.scala	Tue Jul 09 12:32:33 2024 +0200
@@ -22,7 +22,7 @@
 
   object Nat {
     def unapply(bs: Bytes): Option[scala.Int] =
-      if (bs.byte_iterator.forall(b => '0' <= b && b <= '9')) unapply(bs.text)
+      if (bs.byte_iterator.forall(Symbol.is_ascii_digit)) unapply(bs.text)
       else None
     def unapply(s: java.lang.String): Option[scala.Int] =
       s match {
diff -r e066cc867115 -r d1662f1296db src/Pure/PIDE/byte_message.scala
--- 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 = {