# HG changeset patch
# User wenzelm
# Date 1720169702 -7200
# Node ID 8e4731a2a0415dc006c0b8f82a9587c6894c1f1f
# Parent  ddefb18b5b88e79b40a34b87ff214be3cdfcbf02
tuned;

diff -r ddefb18b5b88 -r 8e4731a2a041 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Jul 05 00:21:47 2024 +0200
+++ b/src/Pure/General/scan.scala	Fri Jul 05 10:55:02 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(Bytes.raw(s)) else s
+    if (is_utf8) Bytes.raw(s).text else s
 
   def reader_decode_utf8(reader: Reader[Char], s: String): String =
     reader_decode_utf8(reader_is_utf8(reader), s)
diff -r ddefb18b5b88 -r 8e4731a2a041 src/Tools/jEdit/jedit_main/scala_console.scala
--- a/src/Tools/jEdit/jedit_main/scala_console.scala	Fri Jul 05 00:21:47 2024 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala	Fri Jul 05 10:55:02 2024 +0200
@@ -50,7 +50,7 @@
 
     override def flush(): Unit = {
       val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
-      val str = UTF8.decode_permissive(Bytes.raw(s))
+      val str = Bytes.raw(s).text
       GUI_Thread.later {
         if (global_out == null) java.lang.System.out.print(str)
         else global_out.writeAttrs(null, str)