- coq_makefile: target install now respects the original tree structure

  of the archive to install in coq user-contrib installation directory.
- Relaxed the validity check on identifiers from an error to a warning.
- Added a filtering option to Print LoadPath.
- Support for empty root in option -R.
- Better handling of redundant paths in ml loadpath.
- Makefile's: Added target initplugins and added initplugins to coqbinaries.



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

4 files changed, 61 insertions, 17 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 7ca62dcc8f..00d6dec22f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -63,6 +63,34 @@ type load_path = physical_path list
 let physical_path_of_string s = s
 let string_of_physical_path p = p
 
+(* 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
+
 (* All subdirectories, recursively *)
 
 let exists_dir dir =
diff --git a/lib/system.mli b/lib/system.mli
index 6c607607ff..48e02cb5d2 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -16,6 +16,8 @@
 type physical_path = string
 type load_path = physical_path list
 
+val canonical_path_name : string -> string
+
 val exclude_search_in_dirname : string -> unit
 
 val all_subdirs : unix_path:string -> (physical_path * string list) list
diff --git a/lib/util.ml b/lib/util.ml
index b0e66af05b..3b04e25742 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -309,27 +309,40 @@ let next_utf8 s i =
 
 (* Check the well-formedness of an identifier *)
 
-let check_ident s =
+let check_initial handle j n s =
+  match classify_unicode n with
+  | UnicodeLetter -> ()
+  | _ ->
+      let c = String.sub s 0 j in
+      handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".")
+
+let check_trailing handle i j n s =
+  match classify_unicode n with
+  | UnicodeLetter | UnicodeIdentPart -> ()
+  | _ ->
+      let c = String.sub s i j in
+      handle ("Invalid character '"^c^"' in identifier \""^s^"\".")
+
+let check_ident_gen handle s =
   let i = ref 0 in
   if s <> ".." then try
     let j, n = next_utf8 s 0 in
-    match classify_unicode n with
-    | UnicodeLetter ->
-	i := !i + j;
-	begin try
-	  while true do
-	    let j, n = next_utf8 s !i in
-	    match classify_unicode n with
-	    | UnicodeLetter | UnicodeIdentPart -> i := !i + j
-	    | _ -> error
-		("invalid character "^(String.sub s !i j)^" in identifier "^s)
-	  done
-	with End_of_input -> () end
-    | _ -> error (s^": an identifier should start with a letter")
+    check_initial handle j n s;
+    i := !i + j;
+    try
+      while true do
+	let j, n = next_utf8 s !i in
+	check_trailing handle !i j n s;
+	i := !i + j
+      done
+    with End_of_input -> ()
   with 
-  | End_of_input -> error "The empty string is not an identifier"
-  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence")
-  | Invalid_argument _ -> error (s^": invalid utf8 sequence")
+  | End_of_input -> error "The empty string is not an identifier."
+  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.")
+  | Invalid_argument _ -> error (s^": invalid utf8 sequence.")
+
+let check_ident_soft = check_ident_gen warning
+let check_ident = check_ident_gen error
 
 let lowercase_unicode s unicode =
     match unicode land 0x1F000 with
diff --git a/lib/util.mli b/lib/util.mli
index 8b27e61583..dc6498b15c 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -89,6 +89,7 @@ exception UnsupportedUtf8
 
 val classify_unicode : int -> utf8_status
 val check_ident : string -> unit
+val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
 
 (*s Lists. *)