same_file in Minilib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14439 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 0 deletions

diff --git a/ide/minilib.ml b/ide/minilib.ml
index e5019de04..2182c45e0 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -112,3 +112,26 @@ let canonical_path_name p =
   with Sys_error _ ->
     (* We give up to find a canonical name and just simplify it... *)
     strip_path p
+
+(*
+  checks if two file names refer to the same (existing) file by
+  comparing their device and inode.
+  It seems that under Windows, inode is always 0, so we cannot
+  accurately check if
+
+*)
+(* Optimised for partial application (in case many candidates must be
+   compared to f1). *)
+let same_file f1 =
+  try
+    let s1 = Unix.stat f1 in
+    (fun f2 ->
+      try
+        let s2 = Unix.stat f2 in
+        s1.Unix.st_dev = s2.Unix.st_dev &&
+          if Sys.os_type = "Win32" then f1 = f2
+          else s1.Unix.st_ino = s2.Unix.st_ino
+      with
+          Unix.Unix_error _ -> false)
+  with
+      Unix.Unix_error _ -> (fun _ -> false)