src/Pure/System/standard_system.scala
changeset 39578 b75164153c37
parent 39522 01aade784da9
child 39582 a873158542d0
     1.1 --- a/src/Pure/System/standard_system.scala	Tue Sep 21 21:51:26 2010 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Tue Sep 21 21:53:15 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  import java.util.regex.Pattern
     1.5  import java.util.Locale
     1.6  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
     1.7 -  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.8 +  BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.9    File, FileFilter, IOException}
    1.10  
    1.11  import scala.io.{Source, Codec}
    1.12 @@ -77,24 +77,19 @@
    1.13  
    1.14    /* basic file operations */
    1.15  
    1.16 -  def with_tmp_file[A](prefix: String)(body: File => A): A =
    1.17 +  def slurp(reader: BufferedReader): String =
    1.18    {
    1.19 -    val file = File.createTempFile(prefix, null)
    1.20 -    try { body(file) } finally { file.delete }
    1.21 +    val output = new StringBuilder(100)
    1.22 +    var c = -1
    1.23 +    while ({ c = reader.read; c != -1 }) output += c.toChar
    1.24 +    reader.close
    1.25 +    output.toString
    1.26    }
    1.27  
    1.28 -  def read_file(file: File): String =
    1.29 -  {
    1.30 -    val buf = new StringBuilder(file.length.toInt)
    1.31 -    val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset))
    1.32 -    var c = reader.read
    1.33 -    while (c != -1) {
    1.34 -      buf.append(c.toChar)
    1.35 -      c = reader.read
    1.36 -    }
    1.37 -    reader.close
    1.38 -    buf.toString
    1.39 -  }
    1.40 +  def slurp(stream: InputStream): String =
    1.41 +    slurp(new BufferedReader(new InputStreamReader(stream, charset)))
    1.42 +
    1.43 +  def read_file(file: File): String = slurp(new FileInputStream(file))
    1.44  
    1.45    def write_file(file: File, text: CharSequence)
    1.46    {
    1.47 @@ -103,6 +98,12 @@
    1.48      finally { writer.close }
    1.49    }
    1.50  
    1.51 +  def with_tmp_file[A](prefix: String)(body: File => A): A =
    1.52 +  {
    1.53 +    val file = File.createTempFile(prefix, null)
    1.54 +    try { body(file) } finally { file.delete }
    1.55 +  }
    1.56 +
    1.57    // FIXME handle (potentially cyclic) directory graph
    1.58    def find_files(start: File, ok: File => Boolean): List[File] =
    1.59    {
    1.60 @@ -138,7 +139,7 @@
    1.61    def process_output(proc: Process): (String, Int) =
    1.62    {
    1.63      proc.getOutputStream.close
    1.64 -    val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
    1.65 +    val output = slurp(proc.getInputStream)
    1.66      val rc =
    1.67        try { proc.waitFor }
    1.68        finally {