Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un chemin Unix à un chemin Coq

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

4 files changed, 34 insertions, 22 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7262362ec8..b50d3af4b3 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -40,20 +40,23 @@ let load_rcfile() =
   else 
     if Options.is_verbose() then mSGNL [< 'sTR"Skipping rcfile loading." >]
 
+let add_ml_include s =
+  Mltop.dir_ml_dir s
+
 (* Puts dir in the path of ML and in the LoadPath *)
-let add_include s =
+let add_include s alias =
   Mltop.dir_ml_dir s;
-  Library.add_path s
+  Library.add_path s alias
 
-let add_rec_include s = 
-  let subdirs = all_subdirs s in
+let add_rec_include s alias = 
+  let subdirs = all_subdirs s (Some alias) in
   List.iter (fun lpe -> Mltop.dir_ml_dir lpe.directory) subdirs;
   List.iter Library.add_load_path_entry subdirs
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
-let push_include s = includes := (s,false) :: !includes
-let push_rec_include s = includes := (s,true) :: !includes
+let push_include (s, alias) = includes := (s,alias,false) :: !includes
+let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
 (* Because find puts "./" and the loadpath is not nicely pretty-printed *)
 let hm2 s = 
@@ -67,22 +70,23 @@ let init_load_path () =
   if Coq_config.local then begin
     (* local use (no installation) *)
     List.iter 
-      (fun s -> add_include (Filename.concat Coq_config.coqtop s))
+      (fun s -> add_include (Filename.concat Coq_config.coqtop s) ["Coq"])
       ["states"; "dev"];
-    add_rec_include (Filename.concat Coq_config.coqtop "theories");
-    add_include (Filename.concat Coq_config.coqtop "tactics");
-    add_rec_include (Filename.concat Coq_config.coqtop "contrib");
+    add_rec_include (Filename.concat Coq_config.coqtop "theories") ["Coq"];
+    add_include (Filename.concat Coq_config.coqtop "tactics") ["Coq"];
+    add_rec_include (Filename.concat Coq_config.coqtop "contrib") ["Coq"];
   end else begin
     (* default load path; variable COQLIB overrides the default library *)
     let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
-    add_rec_include coqlib
+    add_rec_include coqlib ["Coq"]
   end;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
-  add_include camlp4;
-  add_include ".";
+  add_ml_include camlp4;
+  add_include "." ["Scratch"];
   (* additional loadpath, given with -I -include -R options *)
   List.iter 
-    (fun (s,reci) -> if reci then add_rec_include s else add_include s)
+    (fun (s,alias,reci) ->
+       if reci then add_rec_include s alias else add_include s alias)
     (List.rev !includes);
   includes := []
 
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 7baa825bee..86b2c9b64e 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -11,7 +11,7 @@ val set_rcuser : string -> unit
 val no_load_rc : unit -> unit
 val load_rcfile : unit -> unit
 
-val push_include : string -> unit
-val push_rec_include : string -> unit
+val push_include : string * Names.dir_path -> unit
+val push_rec_include : string * Names.dir_path -> unit
 
 val init_load_path : unit -> unit
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 0c81359cbf..e1ed881930 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -36,7 +36,7 @@ open Vernacinterp
 let coq_mlpath_copy = ref []
 let keep_copy_mlpath s = 
   let dir = glob s in
-  let lpe = { directory = dir; root_dir = dir; relative_subdir = "" } in
+  let lpe = { directory = dir; root_dir = dir; relative_subdir = [] } in
   coq_mlpath_copy := lpe :: !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
@@ -125,7 +125,7 @@ let dir_ml_dir s =
 
 (* For Rec Add ML Path *)
 let rdir_ml_dir dir = 
-  List.iter (fun lpe -> dir_ml_dir lpe.directory) (all_subdirs dir)
+  List.iter (fun lpe -> dir_ml_dir lpe.directory) (all_subdirs dir None)
 
 (* convertit un nom quelconque en nom de fichier ou de module *) 
 let mod_of_name name =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3e34733f50..4277921477 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -165,7 +165,11 @@ let _ =
 let _ = 
   add "ADDPATH"
     (function 
-       | [VARG_STRING dir] -> (fun () -> add_path dir)
+       | [VARG_STRING dir] ->
+	   let alias = Filename.basename dir in
+	   if alias = "" then
+	     error ("Cannot map "^dir^" to a root of Coq library");
+	   (fun () -> add_path dir [alias])
        | _ -> bad_vernac_args "ADDPATH")
 
 (* For compatibility *)
@@ -178,7 +182,11 @@ let _ =
 let _ = 
   add "RECADDPATH"
     (function 
-       | [VARG_STRING dir] -> (fun () -> rec_add_path dir)
+       | [VARG_STRING dir] ->
+	   let alias = Filename.basename dir in
+	   if alias = "" then
+	     error ("Cannot map "^dir^" to a root of Coq library");
+	   (fun () -> rec_add_path dir [alias])
        | _ -> bad_vernac_args "RECADDPATH")
 
 (* For compatibility *)
@@ -284,9 +292,9 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] ->
 	   let s = string_of_id id in
-	   let {relative_subdir = dir},_ = 
+	   let lpe,_ = 
 	     System.find_file_in_path (Library.get_load_path ()) (s^".v") in
-	   fun () -> Lib.start_module ((parse_loadpath dir)@[s])
+	   fun () -> Lib.start_module (lpe.relative_subdir @ [s])
        | _ -> bad_vernac_args "BeginModule")
 
 let _ =