# HG changeset patch
# User wenzelm
# Date 1720033913 -7200
# Node ID d1240adc30ce65e6f6a7e9ec2d7170965821c587
# Parent  d334f158442bf6447df4f971a7c1b120c484fbe2
clarified signature, following 43323d886ea3;

diff -r d334f158442b -r d1240adc30ce src/Pure/General/bytes.scala
--- 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
diff -r d334f158442b -r d1240adc30ce src/Pure/General/utf8.scala
--- 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)
diff -r d334f158442b -r d1240adc30ce src/Pure/System/web_app.scala
--- 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