# HG changeset patch
# User wenzelm
# Date 1718222384 -7200
# Node ID d395b7e14102dd5559613a794f6983c6228d3cc5
# Parent  54a83e8e447bf15972295bd8a02c033816e0c2d1
clarified signature;

diff -r 54a83e8e447b -r d395b7e14102 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jun 12 21:56:01 2024 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jun 12 21:59:44 2024 +0200
@@ -163,7 +163,7 @@
 
   /* elements: signed Byte or unsigned Char */
 
-  def iterator: Iterator[Byte] =
+  def byte_iterator: Iterator[Byte] =
     for (i <- (offset until (offset + length)).iterator)
       yield bytes(i)
 
@@ -209,7 +209,7 @@
 
   def text: String =
     if (is_empty) ""
-    else if (iterator.forall((b: Byte) => b >= 0)) {
+    else if (byte_iterator.forall(_ >= 0)) {
       new String(bytes, offset, length, UTF8.charset)
     }
     else UTF8.decode_permissive_bytes(this)
diff -r 54a83e8e447b -r d395b7e14102 src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Wed Jun 12 21:56:01 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Wed Jun 12 21:59:44 2024 +0200
@@ -79,7 +79,7 @@
   /* hybrid messages: line or length+block (restricted content) */
 
   private def is_length(msg: Bytes): Boolean =
-    !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
+    !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
 
   private def is_terminated(msg: Bytes): Boolean =
     msg.size match {
@@ -95,7 +95,7 @@
 
     val n = msg.size
     write(stream,
-      (if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
+      (if (n > 100 || msg.byte_iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
         List(msg, Bytes.newline))
     flush(stream)
   }