# HG changeset patch
# User wenzelm
# Date 1718116793 -7200
# Node ID 5a555acad203f8d8fbbb8be2811f2d48e742f8be
# Parent  e5a6b3f1f3774c568ae8d4a08ef8f4f464081eae
clarified signature (again);

diff -r e5a6b3f1f377 -r 5a555acad203 src/Pure/General/bytes.scala
--- 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
 
 
diff -r e5a6b3f1f377 -r 5a555acad203 src/Pure/General/utf8.scala
--- 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)