src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Fri Jun 28 11:09:58 2024 +0200
+++ b/src/Pure/General/file.scala	Fri Jun 28 11:37:13 2024 +0200
@@ -205,13 +205,12 @@
   def read(path: Path): String = read(path.file)
 
 
-  def read_stream(reader: BufferedReader): String = {
-    val output = new StringBuilder(100)
-    var c = -1
-    while ({ c = reader.read; c != -1 }) output += c.toChar
-    reader.close()
-    output.toString
-  }
+  def read_stream(reader: BufferedReader): String =
+    Library.string_builder(hint = 100) { output =>
+      var c = -1
+      while ({ c = reader.read; c != -1 }) output += c.toChar
+      reader.close()
+    }
 
   def read_stream(stream: InputStream): String =
     read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))