# HG changeset patch
# User wenzelm
# Date 1342729972 -7200
# Node ID e544dbcdf097fc37d7fdf0416a63afa323af3ab5
# Parent  04fed0cf775a52fc10e970f82901ad605be31c65
added eq_file / copy_file corresponding to File.eq / File.copy in ML;

diff -r 04fed0cf775a -r e544dbcdf097 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Thu Jul 19 20:52:17 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Thu Jul 19 22:32:52 2012 +0200
@@ -123,6 +123,27 @@
     finally { writer.close }
   }
 
+  def eq_file(file1: File, file2: File): Boolean =
+    file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
+
+  def copy_file(src: File, dst: File) =
+    if (!eq_file(src, dst)) {
+      val in = new FileInputStream(src)
+      try {
+        val out = new FileOutputStream(dst)
+        try {
+          val buf = new Array[Byte](65536)
+          var m = 0
+          do {
+            m = in.read(buf, 0, buf.length)
+            if (m != -1) out.write(buf, 0, m)
+          } while (m != -1)
+        }
+        finally { out.close }
+      }
+      finally { in.close }
+    }
+
   def with_tmp_file[A](prefix: String)(body: File => A): A =
   {
     val file = File.createTempFile(prefix, null)