# HG changeset patch
# User wenzelm
# Date 1719955735 -7200
# Node ID 0e2b09fef3d207b0453480810aceb7fbdba187a2
# Parent  972f7a4cdc0e822f69bf28887159e8cb8c969341
more uniform Bytes.read_stream vs. File.read_stream;

diff -r 972f7a4cdc0e -r 0e2b09fef3d2 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jul 02 23:13:35 2024 +0200
+++ b/src/Pure/General/file.scala	Tue Jul 02 23:28:55 2024 +0200
@@ -204,16 +204,7 @@
   def read(file: JFile): String = Bytes.read(file).text
   def read(path: Path): String = read(path.file)
 
-
-  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)))
+  def read_stream(stream: InputStream): String = Bytes.read_stream(stream).text
 
   def read_gzip(file: JFile): String =
     read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))