1.1 --- a/src/Pure/System/standard_system.scala	Fri Jul 20 22:39:59 2012 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Fri Jul 20 23:16:54 2012 +0200
     1.3 @@ -11,15 +11,11 @@
     1.4  import java.util.regex.Pattern
     1.5  import java.util.Locale
     1.6  import java.net.URL
     1.7 -import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
     1.8 -  BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.9 -  File => JFile, FileFilter, IOException}
    1.10 +import java.io.{File => JFile}
    1.11  import java.nio.charset.Charset
    1.12 -import java.util.zip.GZIPOutputStream
    1.13  
    1.14  import scala.io.Codec
    1.15  import scala.util.matching.Regex
    1.16 -import scala.collection.mutable
    1.17  
    1.18  
    1.19  object Standard_System
    1.20 @@ -100,74 +96,6 @@
    1.21    }
    1.22  
    1.23  
    1.24 -  /* basic file operations */
    1.25 -
    1.26 -  def slurp(reader: BufferedReader): String =
    1.27 -  {
    1.28 -    val output = new StringBuilder(100)
    1.29 -    var c = -1
    1.30 -    while ({ c = reader.read; c != -1 }) output += c.toChar
    1.31 -    reader.close
    1.32 -    output.toString
    1.33 -  }
    1.34 -
    1.35 -  def slurp(stream: InputStream): String =
    1.36 -    slurp(new BufferedReader(new InputStreamReader(stream, charset)))
    1.37 -
    1.38 -  def read_file(file: JFile): String = slurp(new FileInputStream(file))
    1.39 -
    1.40 -  def write_file(file: JFile, text: CharSequence, zip: Boolean = false)
    1.41 -  {
    1.42 -    val stream1 = new FileOutputStream(file)
    1.43 -    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    1.44 -    val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
    1.45 -    try { writer.append(text) }
    1.46 -    finally { writer.close }
    1.47 -  }
    1.48 -
    1.49 -  def eq_file(file1: JFile, file2: JFile): Boolean =
    1.50 -    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
    1.51 -
    1.52 -  def copy_file(src: JFile, dst: JFile) =
    1.53 -    if (!eq_file(src, dst)) {
    1.54 -      val in = new FileInputStream(src)
    1.55 -      try {
    1.56 -        val out = new FileOutputStream(dst)
    1.57 -        try {
    1.58 -          val buf = new Array[Byte](65536)
    1.59 -          var m = 0
    1.60 -          do {
    1.61 -            m = in.read(buf, 0, buf.length)
    1.62 -            if (m != -1) out.write(buf, 0, m)
    1.63 -          } while (m != -1)
    1.64 -        }
    1.65 -        finally { out.close }
    1.66 -      }
    1.67 -      finally { in.close }
    1.68 -    }
    1.69 -
    1.70 -  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
    1.71 -  {
    1.72 -    val file = JFile.createTempFile(prefix, null)
    1.73 -    file.deleteOnExit
    1.74 -    try { body(file) } finally { file.delete }
    1.75 -  }
    1.76 -
    1.77 -  // FIXME handle (potentially cyclic) directory graph
    1.78 -  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
    1.79 -  {
    1.80 -    val files = new mutable.ListBuffer[JFile]
    1.81 -    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
    1.82 -    def find_entry(entry: JFile)
    1.83 -    {
    1.84 -      if (ok(entry)) files += entry
    1.85 -      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
    1.86 -    }
    1.87 -    find_entry(start)
    1.88 -    files.toList
    1.89 -  }
    1.90 -
    1.91 -
    1.92    /* shell processes */
    1.93  
    1.94    def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    1.95 @@ -188,7 +116,7 @@
    1.96    def process_output(proc: Process): (String, Int) =
    1.97    {
    1.98      proc.getOutputStream.close
    1.99 -    val output = slurp(proc.getInputStream)
   1.100 +    val output = File.read(proc.getInputStream)
   1.101      val rc =
   1.102        try { proc.waitFor }
   1.103        finally {