diff -r ab4badc7db7f -r 1f1ce661c71c src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sat Jun 15 22:43:01 2024 +0200 +++ b/src/Pure/General/bytes.scala Sat Jun 15 23:24:24 2024 +0200 @@ -410,10 +410,18 @@ def text: String = if (is_empty) "" - else if (byte_iterator.forall(_ >= 0)) { - new String(make_array, UTF8.charset) + else { + var i = 0L + var utf8 = false + while (i < size && !utf8) { + if (byte_unchecked(i) < 0) { utf8 = true } + i += 1 + } + utf8 + + if (utf8) UTF8.decode_permissive_bytes(this) + else new String(make_array, UTF8.charset) } - else UTF8.decode_permissive_bytes(this) def wellformed_text: Option[String] = try {