Lissage de la gestion des chemins de chargement de fichiers :

- Option -R fait maintenant des Import à tous les niveaux de la
  hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche.
- Option -I rend maintenant possible l'accès aux sous-répertoires via
  les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il
  rend récursivement visibles les noms non qualifiés.
- Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir.
- Ajout option -exclude-dir pour exclure certains sous-répertoires de
  la descente récursive de -R.
- Amélioration message de localisation pour fichiers venant d'un "state".
- Adaptation du checker (et ajout du test check_coq_overwriting qui
  semblait involontairement oublié dans l'option -R).


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

4 files changed, 44 insertions, 31 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 83a4703a24..7e92b804ca 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -72,10 +72,12 @@ 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_include d p = push_include (d,p)
-let set_rec_include d p = check_coq_overwriting p; push_rec_include (d,p)
-let set_default_include d = set_include d Nameops.default_root_prefix
-let set_default_rec_include d = set_rec_include d Nameops.default_root_prefix
+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 set_rec_include d p =
+  let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
  
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
@@ -187,15 +189,22 @@ let parse_args is_ide =
     | "-impredicative-set" :: rem -> 
         set_engagement Declarations.ImpredicativeSet; parse rem
 
+    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
+    | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: p :: rem ->set_rec_include d (dirpath_of_string p);parse rem
+    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
+    | "-R" :: d :: "-as" :: [] -> usage ()
+    | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
     | "-top" :: [] -> usage ()
 
+    | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem
+    | "-exclude-dir" :: [] -> usage ()
+
     | "-notop" :: rem -> unset_toplevel_name (); parse rem
     | "-q" :: rem -> no_load_rc (); parse rem
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 71369f0ab8..c64807db12 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -108,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 !coq_mlpath_copy s in
+        let _,gname = where_in_path true !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	  Dynlink.add_interfaces 
@@ -145,7 +145,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
   if exists_dir dir then
     begin
       add_ml_dir dir;
-      Library.add_load_path (dir,coq_dirpath)
+      Library.add_load_path true (dir,coq_dirpath)
     end
   else
     msg_warning [< str ("Cannot open " ^ dir) >]
@@ -159,19 +159,18 @@ let convert_string d =
     failwith "caught"
 
 let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
-  let dirs = all_subdirs dir in
-  let prefix = Names.repr_dirpath coq_dirpath in
-  if dirs <> [] then
+  if exists_dir dir then
+    let dirs = all_subdirs dir in
+    let prefix = Names.repr_dirpath coq_dirpath in
     let convert_dirs (lp,cp) =
-      (lp,Names.make_dirpath
-            ((List.map convert_string (List.rev cp))@prefix)) in
+      (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
     let dirs = map_succeed convert_dirs dirs in
-    begin
-      List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
-      List.iter Library.add_load_path dirs
-    end
+    List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
+    add_ml_dir dir;
+    List.iter (Library.add_load_path false) dirs;
+    Library.add_load_path true (dir,coq_dirpath)
   else
-    msg_warning [< str ("Cannot open " ^ dir) >]
+    msg_warning (str ("Cannot open " ^ dir))
 
 (* convertit un nom quelconque en nom de fichier ou de module *) 
 let mod_of_name name =
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e00f7808ba..124ce0593e 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -20,10 +20,14 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "Coq options are:\n";
   output_string co
-"  -I dir                 add directory dir in the include path
+"  -I dir -as coqdir      map physical dir to logical coqdir
+  -I dir                 map directory dir to the empty logical path
   -include dir           (idem)
-  -R dir coqdir          recursively map physical dir to logical coqdir 
+  -R dir -as coqdir      recursively map physical dir to logical coqdir 
+  -R dir coqdir          (idem)
   -top coqdir            set the toplevel name to be coqdir instead of Top
+  -notop    r            set the toplevel name to be the empty logical path
+  -exclude-dir f         exclude subdirectories named f for option -R
 
   -inputstate f          read state from file f.coq
   -is f                  (idem)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d1003bd830..7ccfe526d8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -180,12 +180,12 @@ let show_match id =
 (* "Print" commands *)
 
 let print_path_entry (s,l) =
-  (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l))
+  (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
 
 let print_loadpath () =
   let l = Library.get_full_load_paths () in
-  msgnl (Pp.t (str "Physical path:                                 " ++
-		 tab () ++ str "Logical Path:" ++ fnl () ++ 
+  msgnl (Pp.t (str "Logical Path:                 " ++
+		 tab () ++ str "Physical path:" ++ fnl () ++
 		 prlist_with_sep pr_fnl print_path_entry l))
 
 let print_modules () =
@@ -232,7 +232,7 @@ let dump_universes s =
 
 let locate_file f =
   try
-    let _,file = System.where_in_path (Library.get_load_paths ()) f in
+    let _,file = System.where_in_path false (Library.get_load_paths ()) f in
     msgnl (str file)
   with Not_found -> 
     msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -240,24 +240,25 @@ let locate_file f =
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->
-      msgnl(pr_dirpath fulldir ++ str " has been loaded from file" ++ fnl () ++
-      str file)
+      msgnl (hov 0
+	(pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
+	 str file))
   | Library.LibInPath, fulldir, file ->
-      msgnl(pr_dirpath fulldir ++ str " is bound to file " ++ str file)
+      msgnl (hov 0
+	(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
 let msg_notfound_library loc qid = function
   | Library.LibUnmappedDir ->
       let dir = fst (repr_qualid qid) in
       user_err_loc (loc,"locate_library",
-        str "Cannot find a physical path bound to logical path " ++
+        strbrk "Cannot find a physical path bound to logical path " ++
            pr_dirpath dir ++ fnl ())
   | Library.LibNotFound ->
-      msgnl (hov 0 
-	(str"Unable to locate library" ++ spc () ++ pr_qualid qid))
+      msgnl (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid))
   | e -> assert false
 
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
-  try msg_found_library (Library.locate_qualified_library qid)
+  try msg_found_library (Library.locate_qualified_library false qid)
   with e -> msg_notfound_library loc qid e
 
 let print_located_module r = 
@@ -570,7 +571,7 @@ let vernac_end_segment lid =
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library qid) in dp) qidl in
+  let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library false qid) in dp) qidl in
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl;
     Library.require_library qidl import