# HG changeset patch
# User wenzelm
# Date 1285098795 -7200
# Node ID b75164153c3745e9465a86a148dff23947989ece
# Parent  51bcd60039844bbf3b19440b1b8979cecb0ceee6
added Standard_System.slurp convenience;
tuned;

diff -r 51bcd6003984 -r b75164153c37 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Tue Sep 21 21:51:26 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Tue Sep 21 21:53:15 2010 +0200
@@ -9,7 +9,7 @@
 import java.util.regex.Pattern
 import java.util.Locale
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
-  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
+  BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
   File, FileFilter, IOException}
 
 import scala.io.{Source, Codec}
@@ -77,24 +77,19 @@
 
   /* basic file operations */
 
-  def with_tmp_file[A](prefix: String)(body: File => A): A =
+  def slurp(reader: BufferedReader): String =
   {
-    val file = File.createTempFile(prefix, null)
-    try { body(file) } finally { file.delete }
+    val output = new StringBuilder(100)
+    var c = -1
+    while ({ c = reader.read; c != -1 }) output += c.toChar
+    reader.close
+    output.toString
   }
 
-  def read_file(file: File): String =
-  {
-    val buf = new StringBuilder(file.length.toInt)
-    val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset))
-    var c = reader.read
-    while (c != -1) {
-      buf.append(c.toChar)
-      c = reader.read
-    }
-    reader.close
-    buf.toString
-  }
+  def slurp(stream: InputStream): String =
+    slurp(new BufferedReader(new InputStreamReader(stream, charset)))
+
+  def read_file(file: File): String = slurp(new FileInputStream(file))
 
   def write_file(file: File, text: CharSequence)
   {
@@ -103,6 +98,12 @@
     finally { writer.close }
   }
 
+  def with_tmp_file[A](prefix: String)(body: File => A): A =
+  {
+    val file = File.createTempFile(prefix, null)
+    try { body(file) } finally { file.delete }
+  }
+
   // FIXME handle (potentially cyclic) directory graph
   def find_files(start: File, ok: File => Boolean): List[File] =
   {
@@ -138,7 +139,7 @@
   def process_output(proc: Process): (String, Int) =
   {
     proc.getOutputStream.close
-    val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
+    val output = slurp(proc.getInputStream)
     val rc =
       try { proc.waitFor }
       finally {