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.

3 files changed, 7 insertions, 14 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b7f1e4a197..4031a161b8 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 14d2bcea41..a0cd618e99 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 8efcccaaae..ec81a3f1ae 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