diff -r b439582efc8a -r 43323d886ea3 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Wed Jul 03 20:18:36 2024 +0200 +++ b/src/Pure/General/scan.scala Wed Jul 03 20:35:10 2024 +0200 @@ -436,7 +436,7 @@ reader.isInstanceOf[Byte_Reader] def reader_decode_utf8(is_utf8: Boolean, s: String): String = - if (is_utf8) UTF8.decode_permissive(s) else s + if (is_utf8) UTF8.decode_permissive(Bytes.raw(s)) else s def reader_decode_utf8(reader: Reader[Char], s: String): String = reader_decode_utf8(reader_is_utf8(reader), s)