[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.

1 files changed, 29 insertions, 5 deletions

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