diff options
Diffstat (limited to 'ide/minilib.ml')
-rw-r--r-- | ide/minilib.ml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml index dcadc81f5..71956cf8f 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -74,3 +74,31 @@ let home = let coqlib = ref "" let coqtop_path = ref "" + +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p |