src/Pure/System/standard_system.scala
changeset 48359 e544dbcdf097
parent 48277 f14e564fca1a
child 48373 527e2bad7cca
     1.1 --- a/src/Pure/System/standard_system.scala	Thu Jul 19 20:52:17 2012 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Thu Jul 19 22:32:52 2012 +0200
     1.3 @@ -123,6 +123,27 @@
     1.4      finally { writer.close }
     1.5    }
     1.6  
     1.7 +  def eq_file(file1: File, file2: File): Boolean =
     1.8 +    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
     1.9 +
    1.10 +  def copy_file(src: File, dst: File) =
    1.11 +    if (!eq_file(src, dst)) {
    1.12 +      val in = new FileInputStream(src)
    1.13 +      try {
    1.14 +        val out = new FileOutputStream(dst)
    1.15 +        try {
    1.16 +          val buf = new Array[Byte](65536)
    1.17 +          var m = 0
    1.18 +          do {
    1.19 +            m = in.read(buf, 0, buf.length)
    1.20 +            if (m != -1) out.write(buf, 0, m)
    1.21 +          } while (m != -1)
    1.22 +        }
    1.23 +        finally { out.close }
    1.24 +      }
    1.25 +      finally { in.close }
    1.26 +    }
    1.27 +
    1.28    def with_tmp_file[A](prefix: String)(body: File => A): A =
    1.29    {
    1.30      val file = File.createTempFile(prefix, null)