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.

7 files changed, 19 insertions, 20 deletions

diff --git a/library/library.ml b/library/library.ml
index 6d7b0f603..f5c7f6335 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 26af809e7..d35dca212 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 3251b8c60..c2c689af7 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. *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 4df9603dc..06bf955c8 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -104,9 +104,7 @@ let schedule_vio_compilation j fs =
     let f =
       if Filename.check_suffix f ".vio" then Filename.chop_extension f
       else f in
-    let paths = Loadpath.get_paths () in
-    let _, long_f_dot_v =
-      System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+    let long_f_dot_v = Loadpath.locate_file (f^".v") in
     let aux = Aux_file.load_aux_file_for long_f_dot_v in
     let eta =
       try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b7f1e4a19..4031a161b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -162,6 +162,7 @@ let add_load_vernacular verb s =
 let load_vernacular () =
   List.iter
     (fun (s,b) ->
+      let s = Loadpath.locate_file s in
       if Flags.do_beautify () then
 	with_option beautify_file (Vernac.load_vernac b) s
       else
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 14d2bcea4..a0cd618e9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -97,10 +97,7 @@ let user_error loc s = Errors.user_err_loc (loc,"_",str s)
    Note: we could use only one thanks to seek_in, but seeking on and on in
    the file we parse seems a bit risky to me.  B.B.  *)
 
-let open_file_twice_if verbosely fname =
-  let paths = Loadpath.get_paths () in
-  let _,longfname =
-    find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
@@ -206,19 +203,17 @@ let rec vernac_com verbose checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+        let fname = CUnix.make_suffix fname ".v" in
+        let f = Loadpath.locate_file fname in
 	let st = save_translator_coqdoc () in
 	if !Flags.beautify_file then
 	  begin
-            let paths = Loadpath.get_paths () in
-            let _,f = find_file_in_path ~warn:(Flags.is_verbose())
-	      paths
-	      (CUnix.make_suffix fname ".v") in
 	    chan_beautify := open_out (f^beautify_suffix);
 	    Pp.comments := []
           end;
 	begin
 	  try
-            read_vernac_file verbosely (CUnix.make_suffix fname ".v");
+            read_vernac_file verbosely f;
 	    restore_translator_coqdoc st;
 	  with reraise ->
             let reraise = Errors.push reraise in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8efcccaaa..ec81a3f1a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -365,8 +365,7 @@ let dump_universes sorted s =
 (* "Locate" commands *)
 
 let locate_file f =
-  let paths = Loadpath.get_paths () in
-  let _, file = System.find_file_in_path ~warn:false paths f in
+  let file = Flags.silently Loadpath.locate_file f in
   str file
 
 let msg_found_library = function
@@ -1845,9 +1844,7 @@ let vernac_load interp fname =
     Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in
   let input =
-    let paths = Loadpath.get_paths () in
-    let _,longfname =
-      System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+    let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
     Pcoq.Gram.parsable (Stream.of_channel in_chan) in
   try while true do interp (snd (parse_sentence input)) done