src/Pure/library.scala

--- a/src/Pure/library.scala	Fri Jun 28 11:09:58 2024 +0200
+++ b/src/Pure/library.scala	Fri Jun 28 11:37:13 2024 +0200
@@ -194,12 +194,8 @@
       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
       else throw new IndexOutOfBoundsException
 
-    override def toString: String = {
-      val buf = new StringBuilder(length)
-      for (i <- 0 until length)
-        buf.append(charAt(i))
-      buf.toString
-    }
+    override def toString: String =
+      string_builder(hint = length) { buf => for (i <- 0 until length) buf.append(charAt(i)) }
   }
 
   class Line_Termination(text: CharSequence) extends CharSequence {