diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-01-29 03:18:56 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-01-29 03:24:55 +0100 |
commit | 1ee761a2b315970a0169c1e99f4729f11ac1eea1 (patch) | |
tree | e73379aa3785a99fe44598d147991aadf74fe79f /vernac/mltop.mli | |
parent | d0e05a1964fb2af093ac2a15a75bb84d342bf1ad (diff) |
[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.
Diffstat (limited to 'vernac/mltop.mli')
-rw-r--r-- | vernac/mltop.mli | 24 |
1 files changed, 18 insertions, 6 deletions
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 |