From 1ee761a2b315970a0169c1e99f4729f11ac1eea1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.mli | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'vernac/mltop.mli')

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
-- 
cgit v1.2.3