diff -r b439582efc8a -r 43323d886ea3 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jul 03 20:18:36 2024 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jul 03 20:35:10 2024 +0200
@@ -10,6 +10,7 @@
 import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream,
   InputStream, OutputStream, File => JFile}
 import java.nio.ByteBuffer
+import java.nio.charset.StandardCharsets.ISO_8859_1
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
 import java.util.Arrays
@@ -45,6 +46,10 @@
 
   val empty: Bytes = reuse_array(new Array(0))
 
+  def raw(s: String): Bytes =
+    if (s.isEmpty) empty
+    else Builder.use(hint = s.length) { builder => builder += s.getBytes(ISO_8859_1) }
+
   def apply(s: String): Bytes =
     if (s.isEmpty) empty
     else Builder.use(hint = s.length) { builder => builder += s }
@@ -131,21 +136,6 @@
   def append(path: Path, bytes: Bytes): Unit = append(path.file, bytes)
 
 
-  /* vector of short unsigned integers */
-
-  trait Vec {
-    def size: Long
-    def apply(i: Long): Char
-  }
-
-  class Vec_String(string: String) extends Vec {
-    override def size: Long = string.length.toLong
-    override def apply(i: Long): Char =
-      if (0 <= i && i < size) string(i.toInt)
-      else throw new IndexOutOfBoundsException
-  }
-
-
   /* incremental builder: unsynchronized! */
 
   object Builder {
@@ -294,7 +284,7 @@
   protected val chunk0: Array[Byte],
   protected val offset: Long,
   val size: Long
-) extends Bytes.Vec with YXML.Source {
+) extends YXML.Source {
   bytes =>
 
   assert(
@@ -499,7 +489,7 @@
       }
       utf8
 
-      if (utf8) UTF8.decode_permissive_bytes(bytes)
+      if (utf8) UTF8.decode_permissive(bytes)
       else new String(make_array, UTF8.charset)
     }