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.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'library/loadpath.mli') 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 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.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'library/loadpath.mli') diff --git a/library/loadpath.mli b/library/loadpath.mli index c2c689af70..269e28e0b5 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -27,9 +27,6 @@ val logical : t -> DirPath.t val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val get_paths : unit -> CUnix.physical_path list -(** Same as [get_load_paths] but only get the physical part. *) - val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit (** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) -- cgit v1.2.3 From d55676344c8dc0d9a87b2ef12ec2348281db4bf5 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 14:10:31 +0100 Subject: Move the From logic to Loadpath.expand_path. --- library/loadpath.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/loadpath.mli') diff --git a/library/loadpath.mli b/library/loadpath.mli index 269e28e0b5..732f6349fb 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -42,7 +42,7 @@ val find_load_path : CUnix.physical_path -> t val is_in_load_paths : CUnix.physical_path -> bool (** Whether a physical path is currently bound. *) -val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list +val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list (** Given a relative logical path, associate the list of absolute physical and logical paths which are possible matches of it. *) -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- library/loadpath.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/loadpath.mli') diff --git a/library/loadpath.mli b/library/loadpath.mli index 269e28e0b5..49ffc11480 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*