Creation of ide/project_file.ml4

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

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