# HG changeset patch
# User wenzelm
# Date 1120050813 -7200
# Node ID 1776d276f8480f8ba9fe2c34ad714a73535aec1d
# Parent  0eda2f8a74aa803031138d2793e35ee0de3e3e87
added eq;
improved copy/copy_dir: only copy if non-eq;

diff -r 0eda2f8a74aa -r 1776d276f848 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Jun 29 15:13:32 2005 +0200
+++ b/src/Pure/General/file.ML	Wed Jun 29 15:13:33 2005 +0200
@@ -22,6 +22,7 @@
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
+  val eq: Path.T * Path.T -> bool
   val copy: Path.T -> Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
   eqtype info
@@ -121,12 +122,17 @@
 
 end;
 
-fun copy from to =
+fun eq paths =
+  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
+    SOME ids => OS.FileSys.compare ids = EQUAL
+  | NONE => false);
+
+fun copy from to = conditional (not (eq (from, to))) (fn () =>
   let val target = if is_dir to then Path.append to (Path.base from) else to
-  in write target (read from) end;
+  in write target (read from) end);
 
-fun copy_dir from to =
-  (system ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); ());  (* FIXME system_command *)
+fun copy_dir from to = conditional (not (eq (from, to))) (fn () =>
+  (system_command ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); ()))
 
 
 (* use ML files *)