diff options
| author | herbelin | 2000-11-29 11:30:53 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-29 11:30:53 +0000 |
| commit | 123c3a105b69ca63c54976df74cb816437946589 (patch) | |
| tree | fa02c4de0316a6e651da62ec8540eedb178c6302 /library | |
| parent | 7963f0ef1839f575c4a5e3f5ac953e2709bc7a0c (diff) | |
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 16 | ||||
| -rw-r--r-- | library/library.mli | 4 |
2 files changed, 12 insertions, 8 deletions
diff --git a/library/library.ml b/library/library.ml index cd99b603e2..abdce3482f 100644 --- a/library/library.ml +++ b/library/library.ml @@ -17,14 +17,19 @@ let get_load_path () = !load_path let add_load_path_entry lpe = load_path := lpe :: !load_path -let add_path dir = - add_load_path_entry { directory = dir; root_dir = dir; relative_subdir = "" } +let add_path dir coq_dirpath = + if coq_dirpath = [] then anomaly "add_path: empty path in library"; + Nametab.push_library_root (List.hd coq_dirpath); + add_load_path_entry + { directory = dir; root_dir = dir; relative_subdir = coq_dirpath } let remove_path dir = load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path -let rec_add_path dir = - load_path := (all_subdirs dir) @ !load_path +let rec_add_path dir coq_dirpath = + if coq_dirpath = [] then anomaly "add_path: empty path in library"; + Nametab.push_library_root (List.hd coq_dirpath); + load_path := (all_subdirs dir (Some coq_dirpath)) @ !load_path (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) @@ -159,8 +164,7 @@ let rec load_module_from s f = List.iter (load_mandatory_module s) m.module_deps; Global.import m.module_compiled_env; load_objects m.module_declarations; - let dir = parse_loadpath lpe.relative_subdir in - let sp = Names.make_path dir (id_of_string s) CCI in + let sp = Names.make_path lpe.relative_subdir (id_of_string s) CCI in Nametab.push_module sp m.module_nametab; modules_table := Stringmap.add s m !modules_table; m diff --git a/library/library.mli b/library/library.mli index 4ff27b4cd6..4d4a2d19b1 100644 --- a/library/library.mli +++ b/library/library.mli @@ -58,6 +58,6 @@ val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit (*s Global load path *) 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 add_path : unix_path:string -> coq_root:dir_path -> unit +val rec_add_path : unix_path:string -> coq_root:dir_path -> unit val remove_path : string -> unit |