diff options
| -rw-r--r-- | toplevel/coqinit.ml | 11 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 9 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 16 insertions, 10 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index d9cd574a04..258a1135fc 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,13 +59,12 @@ let load_rcfile() = (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = - Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); - if with_ml then - Mltop.add_rec_ml_dir unix_path + let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in + Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init) let add_userlib_path ~unix_path = - Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; - Mltop.add_rec_ml_dir unix_path + Mltop.add_rec_path Mltop.AddRecML ~unix_path + ~coq_root:Nameops.default_root_prefix ~implicit:false (* Options -I, -I-as, and -R of the command line *) let includes = ref [] @@ -108,7 +107,7 @@ let init_load_path () = (* additional loadpath, given with options -Q and -R *) List.iter (fun (unix_path, coq_root, implicit) -> - Mltop.add_rec_path ~unix_path ~coq_root ~implicit) + Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit) (List.rev !includes); (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index f972959453..0a5b92270f 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -182,7 +182,9 @@ let warn_cannot_open_path = CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" (fun unix_path -> str "Cannot open " ++ str unix_path) -let add_rec_path ~unix_path ~coq_root ~implicit = +type add_ml = AddNoML | AddTopML | AddRecML + +let add_rec_path add_ml ~unix_path ~coq_root ~implicit = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in let prefix = Names.DirPath.repr coq_root in @@ -193,7 +195,10 @@ let add_rec_path ~unix_path ~coq_root ~implicit = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let () = add_ml_dir unix_path in + let () = match add_ml with + | AddNoML -> () + | AddTopML -> add_ml_dir unix_path + | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in let add (path, dir) = Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 5d05468241..6633cb9372 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -46,8 +46,10 @@ val dir_ml_use : string -> unit val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit +type add_ml = AddNoML | AddTopML | AddRecML + (** Adds a path to the Coq and ML paths *) -val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit +val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 33a8609a77..48a85b709f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -880,7 +880,7 @@ let expand filename = let vernac_add_loadpath implicit pdir ldiropt = let pdir = expand pdir in let alias = Option.default Nameops.default_root_prefix ldiropt in - Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit + Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) |