more direct File.read_bytes -- avoid cumulative copying of StringBuilder;

--- 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 */