# HG changeset patch
# User wenzelm
# Date 1345746891 -7200
# Node ID f686cb016c0cef153c1a118852f82962434d6605
# Parent  ffdb37019b2f85b04b4f50f32b5054e8ffda00f8
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;

diff -r ffdb37019b2f -r f686cb016c0c src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Aug 23 19:57:55 2012 +0200
+++ b/src/Pure/General/file.scala	Thu Aug 23 20:34:51 2012 +0200
@@ -35,6 +35,29 @@
 
   /* read */
 
+  def read_bytes(file: JFile): Array[Byte] =
+  {
+    var i = 0
+    var m = 0
+    val n = file.length.toInt
+    val buf = new Array[Byte](n)
+
+    val stream = new FileInputStream(file)
+    try {
+      do {
+        m = stream.read(buf, i, n - i)
+        if (m != -1) i += m
+      } while (m != -1 && n > i)
+    }
+    finally { stream.close }
+    buf
+  }
+
+  def read(file: JFile): String =
+    new String(read_bytes(file), Standard_System.charset)
+
+  def read(path: Path): String = read(path.file)
+
   def read(reader: BufferedReader): String =
   {
     val output = new StringBuilder(100)
@@ -47,10 +70,6 @@
   def read(stream: InputStream): String =
     read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset)))
 
-  def read(file: JFile): String = read(new FileInputStream(file))
-
-  def read(path: Path): String = read(path.file)
-
 
   /* try_read */