# HG changeset patch
# User wenzelm
# Date 1719575166 -7200
# Node ID 2bbcfcfca0cd08af97590e1ac2562f61b8ac5301
# Parent  ab0dd21dd0cad8bb86e83781a8885b5e313044c5
tuned;

diff -r ab0dd21dd0ca -r 2bbcfcfca0cd src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Jun 28 13:20:18 2024 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 28 13:46:06 2024 +0200
@@ -541,8 +541,7 @@
     if (encode(decoded) == text) decoded
     else {
       val bad = new mutable.ListBuffer[Symbol]
-      for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s))
-        bad += s
+      for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) bad += s
       error("Bad Unicode symbols in text: " + commas_quote(bad))
     }
   }
diff -r ab0dd21dd0ca -r 2bbcfcfca0cd src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Fri Jun 28 13:20:18 2024 +0200
+++ b/src/Pure/General/utf8.scala	Fri Jun 28 13:46:06 2024 +0200
@@ -41,8 +41,7 @@
     var rest = 0
     def flush(): Unit = {
       if (code != -1) {
-        if (rest == 0 && Character.isValidCodePoint(code))
-          buf.appendCodePoint(code)
+        if (rest == 0 && Character.isValidCodePoint(code)) buf.appendCodePoint(code)
         else buf.append('\uFFFD')
         code = -1
         rest = 0