fixed same_file (#1141)

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

2 files changed, 31 insertions, 30 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 4afb677d5..17965558c 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -77,26 +77,18 @@ let version () =
 
 let is_in_coq_lib dir = 
   prerr_endline ("Is it a coq theory ? : "^dir);
-  try
-    let stat = Unix.stat dir in
-      List.exists 
-	(fun s -> 
-	   try
-	     let fdir = Filename.concat 
-	       Coq_config.coqlib 
-	       (Filename.concat "theories" s) 
-	     in
-	       prerr_endline (" Comparing to: "^fdir);
-	       let fstat = Unix.stat fdir in 
-		 (fstat.Unix.st_dev = stat.Unix.st_dev) &&
-		   (fstat.Unix.st_ino = stat.Unix.st_ino) && 
-		   (prerr_endline " YES";true)
-	   with _ -> prerr_endline " No(because of a local exn)";false
-	)
-	Coq_config.theories_dirs
-  with _ -> prerr_endline " No(because of a global exn)";false
-
-let is_in_loadpath dir = Library.is_in_load_paths (System.physical_path_of_string dir)
+  let is_same_file = same_file dir in
+  List.exists 
+    (fun s -> 
+      let fdir =
+        Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in
+      prerr_endline (" Comparing to: "^fdir);
+      if is_same_file fdir then (prerr_endline " YES";true)
+      else (prerr_endline"NO";false))
+    Coq_config.theories_dirs
+
+let is_in_loadpath dir =
+  Library.is_in_load_paths (System.physical_path_of_string dir)
 
 let is_in_coq_path f = 
   try 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 27c773410..7893590ab 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -267,7 +267,7 @@ let run_command f c =
 
 let browse f url =
   let l,r = !current.cmd_browse in
-  let (s,res) = run_command f (l ^ url ^ r) in
+  let (_s,_res) = run_command f (l ^ url ^ r) in
   ()
 
 let url_for_keyword =
@@ -306,18 +306,27 @@ let tab = Glib.Utf8.to_unichar "\t" (ref 0)
 
 
 (*
-  checks if two file names refer to the same (existing) file
-*)
+  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 
 
-let same_file f1 f2 =
+*)
+(* Optimised for partial application (in case many candidates must be
+   compared to f1). *)
+let same_file f1 =
   try
-    let s1 = Unix.stat f1
-    and s2 = Unix.stat f2 
-    in
-      (s1.Unix.st_dev = s2.Unix.st_dev) &&
-	(s1.Unix.st_ino = s2.Unix.st_ino) 
+    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 _ -> false
+      Unix.Unix_error _ -> (fun _ -> false)
 
 let absolute_filename f =
   if Filename.is_relative f then