From 1ee761a2b315970a0169c1e99f4729f11ac1eea1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jan 2018 03:18:56 +0100 Subject: [toplevel] Refactor load path handling. We refactor top-level load path handling. This is in preparation to make load paths become local to a particular document. To this effect, we introduce a new data type `coq_path` that includes the full specification of a load path: ``` type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { unix_path : string; (* Filesystem path contaning vo/ml files *) coq_path : Names.DirPath.t; (* Coq prefix for the path *) implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) } type coq_path_spec = | VoPath of vo_path_spec | MlPath of string type coq_path = { path_spec: coq_path_spec; recursive: bool; } ``` Then, initialization of load paths is split into building a list of load paths and actually making them effective. A future commit will make thus the list of load paths a parameter for document creation. This API is necessarily internal [for now] thus I don't think a changes entry is needed. --- vernac/mltop.ml | 34 +++++++++++++++++++++++++++++----- vernac/mltop.mli | 24 ++++++++++++++++++------ vernac/vernacentries.ml | 7 +++++-- 3 files changed, 52 insertions(+), 13 deletions(-) (limited to 'vernac') diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 00554e3ba..053b9d070 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -184,10 +184,28 @@ let warn_cannot_open_path = type add_ml = AddNoML | AddTopML | AddRecML -let add_rec_path add_ml ~unix_path ~coq_root ~implicit = +type vo_path_spec = { + unix_path : string; + coq_path : Names.DirPath.t; + implicit : bool; + has_ml : add_ml; +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in if exists_dir unix_path then - let dirs = all_subdirs ~unix_path in - let prefix = Names.DirPath.repr coq_root in + let dirs = if recursive then all_subdirs ~unix_path else [] in + let prefix = Names.DirPath.repr lp.coq_path in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in @@ -195,17 +213,23 @@ let add_rec_path add_ml ~unix_path ~coq_root ~implicit = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let () = match add_ml with + let () = match lp.has_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 - Loadpath.add_load_path unix_path ~implicit coq_root + Loadpath.add_load_path unix_path ~implicit lp.coq_path else warn_cannot_open_path unix_path +let add_coq_path { recursive; path_spec } = match path_spec with + | VoPath lp -> + add_vo_path ~recursive lp + | MlPath dir -> + if recursive then add_rec_ml_dir dir else add_ml_dir dir + (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = if Filename.check_suffix name ".cmo" then diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 324a66d38..e44a7c243 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -42,14 +42,26 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the ML paths *) -val add_ml_dir : string -> unit -val add_rec_ml_dir : string -> unit - +(** Adds a path to the Coq and ML paths *) type add_ml = AddNoML | AddTopML | AddRecML -(** Adds a path to the Coq and ML paths *) -val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit +type vo_path_spec = { + unix_path : string; (* Filesystem path contaning vo/ml files *) + coq_path : Names.DirPath.t; (* Coq prefix for the path *) + implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +val add_coq_path : coq_path -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3358951f4..1a02a22a5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -905,9 +905,11 @@ let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = + let open Mltop in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in - Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit + add_coq_path { recursive = true; + path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } } let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) @@ -915,7 +917,8 @@ let vernac_remove_loadpath path = (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) + let open Mltop in + add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~atts l = let local = make_locality atts.locality in -- cgit v1.2.3