--- a/src/Pure/General/bytes.scala Wed Jul 03 20:59:30 2024 +0200
+++ b/src/Pure/General/bytes.scala Wed Jul 03 21:11:53 2024 +0200
@@ -327,11 +327,13 @@
}
}
+ // signed byte
def byte(i: Long): Byte =
if (0 <= i && i < size) byte_unchecked(i)
else throw new IndexOutOfBoundsException
- def apply(i: Long): Char = (byte(i).toInt & 0xff).toChar
+ // unsigned char
+ def char(i: Long): Char = (byte(i).toInt & 0xff).toChar
protected def subarray_iterator: Iterator[Bytes.Subarray] =
if (is_empty) Iterator.empty
--- a/src/Pure/General/utf8.scala Wed Jul 03 20:59:30 2024 +0200
+++ b/src/Pure/General/utf8.scala Wed Jul 03 21:11:53 2024 +0200
@@ -50,7 +50,7 @@
}
}
for (i <- 0L until size) {
- val c: Char = bytes(i)
+ val c = bytes.char(i)
if (c < 128) { flush(); buf.append(c) }
else if ((c & 0xC0) == 0x80) push(c & 0x3F)
else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
--- a/src/Pure/System/web_app.scala Wed Jul 03 20:59:30 2024 +0200
+++ b/src/Pure/System/web_app.scala Wed Jul 03 21:11:53 2024 +0200
@@ -125,7 +125,7 @@
var sep_ok = true
var sep_i = 0
while (sep_ok && sep_i < sep.length) {
- if (bytes(bytes_i + sep_i) == sep(sep_i)) {
+ if (bytes.char(bytes_i + sep_i) == sep(sep_i)) {
sep_i += 1
} else {
bytes_i += 1