nouveau load path

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

2 files changed, 17 insertions, 21 deletions

diff --git a/library/library.ml b/library/library.ml
index 4a76bff1c..ca4309634 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -3,33 +3,28 @@
 
 open Pp
 open Util
+open System
 open Names
 open Environ
 open Libobject
 open Lib
 
-(*s Load path. Used for commands Add Path, Remove Path, Print Path *)
+(*s Load path. *)
 
-let loadpath_name = "LoadPath"
+let load_path = ref ([] : load_path)
 
-module LoadPath = struct
-  let check s = if not (System.exists_dir s) then warning (s^" was not found")
-  let key = Goptions.PrimaryTable loadpath_name
-  let title = "Load Paths for Coq files"
-  let member_message s b =
-    if b then s^" is declared in the load path for Coq files"
-    else s^" is not declared in the load path for Coq files"
-  let synchronous = false
-end
+let get_load_path () = !load_path
 
-module LoadPathTable = Goptions.MakeStringTable(LoadPath)
+let add_load_path_entry lpe = load_path := lpe :: !load_path
 
-let get_load_path = LoadPathTable.elements
 let add_path dir = 
-  (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#add dir
+  add_load_path_entry { directory = dir; root_dir = dir; relative_subdir = "" }
+
 let remove_path dir =
-  (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#remove dir
-let rec_add_path dir = List.iter add_path (System.all_subdirs dir)
+  load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path
+
+let rec_add_path dir = 
+  load_path := (all_subdirs dir) @ !load_path
 
 (*s Modules on disk contain the following informations (after the magic 
     number, and before the digest). *)
@@ -45,7 +40,7 @@ type module_disk = {
 
 type module_t = {
   module_name : string;
-  module_filename : string;
+  module_filename : load_path_entry * string;
   module_compiled_env : compiled_env;
   module_declarations : library_segment;
   mutable module_opened : bool;
@@ -129,12 +124,12 @@ let load_objects decls =
   segment_iter load_object decls
 
 let rec load_module_from s f =
-  let (fname,ch) = raw_intern_module (get_load_path ()) f in
+  let (lpe,fname,ch) = raw_intern_module (get_load_path ()) f in
   let md = System.marshal_in ch in
   let digest = System.marshal_in ch in
   close_in ch;
   let m = { module_name = md.md_name;
-	    module_filename = fname;
+	    module_filename = (lpe,fname);
 	    module_compiled_env = md.md_compiled_env;
 	    module_declarations = md.md_declarations;
 	    module_opened = false;
diff --git a/library/library.mli b/library/library.mli
index 474669452..cac8767d5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,10 +38,11 @@ val save_module_to : string -> string -> unit
     [module_filename] returns the full filename of a loaded module. *)
 
 val module_segment : string option -> Lib.library_segment
-val module_filename : string -> string
+val module_filename : string -> System.load_path_entry * string
 
 (*s Global load path *)
-val get_load_path : unit -> string list
+val get_load_path : unit -> System.load_path
+val add_load_path_entry : System.load_path_entry -> unit
 val add_path : string -> unit
 val rec_add_path : string -> unit
 val remove_path : string -> unit