diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 4 | ||||
| -rw-r--r-- | library/loadpath.ml | 6 | ||||
| -rw-r--r-- | library/loadpath.mli | 4 |
3 files changed, 11 insertions, 3 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. *) |