- 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, 22 insertions, 15 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fec6b0740..9ada5bff2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -51,7 +51,9 @@ let set_batch_mode () = batch_mode := true
 
 let toplevel_default_name = make_dirpath [id_of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
-let set_toplevel_name dir = toplevel_name := Some dir
+let set_toplevel_name dir =
+  if dir = empty_dirpath then error "Need a non empty toplevel module name";
+  toplevel_name := Some dir
 let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
@@ -68,16 +70,16 @@ let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
-let check_coq_overwriting p = 
-  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
-    error "The \"Coq\" logical root directory is reserved for the Coq library"
-
 let set_default_include d = push_include (d,Nameops.default_root_prefix)
 let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
 let set_include d p =
-  let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p)
+  let p = dirpath_of_string p in
+  Library.check_coq_overwriting p;
+  push_include (d,p)
 let set_rec_include d p =
-  let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
+  let p = dirpath_of_string p in 
+  Library.check_coq_overwriting p;
+  push_rec_include(d,p)
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index dcdc46e8e..685eaba3f 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -47,8 +47,10 @@ open Vernacinterp
 
 (* This path is where we look for .cmo *)
 let coq_mlpath_copy = ref ["."]
-let keep_copy_mlpath path = 
-  coq_mlpath_copy := path :: !coq_mlpath_copy
+let keep_copy_mlpath path =
+  let cpath = canonical_path_name path in
+  let filter path' = (cpath <> canonical_path_name path') in
+  coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = { 
@@ -106,7 +108,7 @@ let dir_ml_load s =
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
-        let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in
+        let _,gname = where_in_path true !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
@@ -310,10 +312,10 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 	     if_verbose
 	       msg (str"[Loading ML file " ++ str fname ++ str" ...");
              load_object mname fname;
-             if_verbose msgnl (str"done]");
+             if_verbose msgnl (str" done]");
              add_loaded_module mname
            with e ->
-	     if_verbose msgnl (str"failed]");
+	     if_verbose msgnl (str" failed]");
 	     raise e
 	 else
 	   if_verbose
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f5603535b..42a06308c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -182,8 +182,11 @@ let show_match id =
 let print_path_entry (s,l) =
   (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
 
-let print_loadpath () =
+let print_loadpath dir =
   let l = Library.get_full_load_paths () in
+  let l = match dir with
+    | None -> l
+    | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in
   msgnl (Pp.t (str "Logical Path:                 " ++
 		 tab () ++ str "Physical path:" ++ fnl () ++
 		 prlist_with_sep pr_fnl print_path_entry l))
@@ -1063,7 +1066,7 @@ let vernac_print = function
   | PrintSectionContext qid -> msg (print_sec_context_typ qid)
   | PrintInspect n -> msg (inspect n)
   | PrintGrammar ent -> Metasyntax.print_grammar ent
-  | PrintLoadPath -> (* For compatibility ? *) print_loadpath ()
+  | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
   | PrintModules -> msg (print_modules ())
   | PrintModule qid -> print_module qid
   | PrintModuleType qid -> print_modtype qid
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8e797a883..d8084c966 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -38,7 +38,7 @@ type printable =
   | PrintSectionContext of reference
   | PrintInspect of int
   | PrintGrammar of string
-  | PrintLoadPath
+  | PrintLoadPath of dir_path option
   | PrintModules
   | PrintModule of reference
   | PrintModuleType of reference