diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 32 | ||||
| -rw-r--r-- | ide/ideutils.ml | 29 |
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 |