From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 29 Sep 2015 10:26:08 +0200
Subject: Remove some uses of Loadpath.get_paths.

The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.

The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.

Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.

Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
---
 library/library.ml   | 4 +---
 library/loadpath.ml  | 6 ++++++
 library/loadpath.mli | 4 ++++
 3 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 6d7b0f603a..f5c7f63358 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -652,9 +652,7 @@ let start_library f =
   ldir
 
 let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
   let ch = System.with_magic_number_check raw_intern_library f in
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 26af809e78..d35dca2125 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -112,3 +112,9 @@ let expand_path dir =
       if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
   in
   aux !load_paths
+
+let locate_file fname =
+  let paths = get_paths () in
+  let _,longfname =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+  longfname
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 3251b8c60c..c2c689af70 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -52,3 +52,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
 val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
 (** As {!expand_path} but uses a filter function instead, and ignores the
     implicit status of loadpaths. *)
+
+val locate_file : string -> string
+(** Locate a file among the registered paths. Do not use this function, as
+    it does not respect the visibility of paths. *)
-- 
cgit v1.2.3