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