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/loadpath.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'library/loadpath.ml')

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


From b248c23b84a96ef692e4a3ded6668733820e1a77 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 30 Sep 2015 06:52:01 +0200
Subject: Unexport Loadpath.get_paths.

---
 library/loadpath.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'library/loadpath.ml')

diff --git a/library/loadpath.ml b/library/loadpath.ml
index d35dca2125..622d390a2c 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -28,8 +28,6 @@ let physical p = p.path_physical
 
 let get_load_paths () = !load_paths
 
-let get_paths () = List.map physical !load_paths
-
 let anomaly_too_many_paths path =
   anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
 
@@ -114,7 +112,7 @@ let expand_path dir =
   aux !load_paths
 
 let locate_file fname =
-  let paths = get_paths () in
+  let paths = List.map physical !load_paths in
   let _,longfname =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
   longfname
-- 
cgit v1.2.3