diff options
Diffstat (limited to 'library/loadpath.ml')
-rw-r--r-- | library/loadpath.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml index 60799a8a7..7c203bc88 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -22,6 +22,9 @@ type t = { let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" +let accessible_paths = + Summary.ref ([] : CUnix.physical_path list) ~name:"ACCPATHS" + let logical p = p.path_logical let physical p = p.path_physical @@ -30,6 +33,8 @@ let get_load_paths () = !load_paths let get_paths () = List.map physical !load_paths +let get_accessible_paths () = !accessible_paths + let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -63,6 +68,9 @@ let add_load_path phys_path isroot coq_path = match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths; + if isroot then + accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc) + (phys_path :: !accessible_paths) (System.all_subdirs phys_path) | [p] -> let dir = p.path_logical in if not (DirPath.equal coq_path dir) |