--- a/src/Pure/General/bytes.scala Tue Jun 11 16:37:17 2024 +0200
+++ b/src/Pure/General/bytes.scala Tue Jun 11 16:39:53 2024 +0200
@@ -114,17 +114,17 @@
def append(path: Path, bytes: Bytes): Unit = append(path.file, bytes)
- /* vector of unsigned integers */
+ /* vector of short unsigned integers */
trait Vec {
def size: Long
- def apply(i: Long): Int
+ def apply(i: Long): Char
}
class Vec_String(string: String) extends Vec {
override def size: Long = string.length.toLong
- override def apply(i: Long): Int =
- if (0 <= i && i < size) string(i.toInt).toInt
+ override def apply(i: Long): Char =
+ if (0 <= i && i < size) string(i.toInt)
else throw new IndexOutOfBoundsException
}
}
@@ -219,8 +219,8 @@
def size: Long = length.toLong
- def apply(i: Long): Int =
- if (0 <= i && i < size) bytes((offset + i).toInt).asInstanceOf[Int] & 0xFF
+ def apply(i: Long): Char =
+ if (0 <= i && i < size) (bytes((offset + i).toInt).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
else throw new IndexOutOfBoundsException
--- a/src/Pure/General/utf8.scala Tue Jun 11 16:37:17 2024 +0200
+++ b/src/Pure/General/utf8.scala Tue Jun 11 16:39:53 2024 +0200
@@ -51,8 +51,8 @@
}
}
for (i <- 0L until size) {
- val c = bytes(i)
- if (c < 128) { flush(); buf.append(c.toChar) }
+ val c: Char = bytes(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)
else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)