src/Pure/System/standard_system.scala
changeset 48359 e544dbcdf097
parent 48277 f14e564fca1a
child 48373 527e2bad7cca
equal deleted inserted replaced
48358:04fed0cf775a 48359:e544dbcdf097
   120     val writer =
   120     val writer =
   121       new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
   121       new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
   122     try { writer.append(text) }
   122     try { writer.append(text) }
   123     finally { writer.close }
   123     finally { writer.close }
   124   }
   124   }
       
   125 
       
   126   def eq_file(file1: File, file2: File): Boolean =
       
   127     file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
       
   128 
       
   129   def copy_file(src: File, dst: File) =
       
   130     if (!eq_file(src, dst)) {
       
   131       val in = new FileInputStream(src)
       
   132       try {
       
   133         val out = new FileOutputStream(dst)
       
   134         try {
       
   135           val buf = new Array[Byte](65536)
       
   136           var m = 0
       
   137           do {
       
   138             m = in.read(buf, 0, buf.length)
       
   139             if (m != -1) out.write(buf, 0, m)
       
   140           } while (m != -1)
       
   141         }
       
   142         finally { out.close }
       
   143       }
       
   144       finally { in.close }
       
   145     }
   125 
   146 
   126   def with_tmp_file[A](prefix: String)(body: File => A): A =
   147   def with_tmp_file[A](prefix: String)(body: File => A): A =
   127   {
   148   {
   128     val file = File.createTempFile(prefix, null)
   149     val file = File.createTempFile(prefix, null)
   129     file.deleteOnExit
   150     file.deleteOnExit