diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/ideutils.ml | 24 | ||||
| -rw-r--r-- | ide/ideutils.mli | 7 | ||||
| -rw-r--r-- | ide/minilib.ml | 23 | ||||
| -rw-r--r-- | ide/minilib.mli | 4 |
5 files changed, 28 insertions, 32 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index aaafb168b..01a0b3221 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1678,7 +1678,7 @@ let load_file handler f = let f = absolute_filename f in try prerr_endline "Loading file starts"; - let is_f = same_file f in + let is_f = Minilib.same_file f in if not (Minilib.list_fold_left_i (fun i found x -> if found then found else let {analyzed_view=av} = x in diff --git a/ide/ideutils.ml b/ide/ideutils.ml index a27a62170..85e195dae 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -337,30 +337,6 @@ let browse_keyword f text = try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) with Not_found -> f ("No documentation found for \""^text^"\".\n") - -(* - 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) - let absolute_filename f = if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f diff --git a/ide/ideutils.mli b/ide/ideutils.mli index fe8936877..23b31e4ae 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -67,13 +67,6 @@ val set_location : (string -> unit) ref val pbar : GRange.progress_bar - -(* - checks if two file names refer to the same (existing) file -*) - -val same_file : string -> string -> bool - (* returns an absolute filename equivalent to given filename *) 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) diff --git a/ide/minilib.mli b/ide/minilib.mli index 2128b7d86..9c8cf0978 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -28,3 +28,7 @@ val coqtop_path : string ref val strip_path : string -> string val canonical_path_name : string -> string + +(** checks if two file names refer to the same (existing) file *) +val same_file : string -> string -> bool + |