# 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 *)