aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-03-31 18:25:45 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-03-31 18:36:21 +0200
commit765510929b2255d9c56fcdfce4a3ea555b07b340 (patch)
tree368fda2d2a4fde7b3f70f6ad8bae6442a8001f07 /library/loadpath.ml
parente52303164660041690f6e05a110ff633007a1dd5 (diff)
A more reasonable implementation of Loadpath.
The new behaviour is simple: either a path is in the loadpaths or it is not. No more wild expansions of paths! This should not affect -R and -Q, but it does change the semantics of -I -as. Still, there are no more users of it and it only does so in a subtle way.
Diffstat (limited to 'library/loadpath.ml')
-rw-r--r--library/loadpath.ml48
1 files changed, 14 insertions, 34 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml
index ab8b0a307..0f7c2fb46 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -93,47 +93,27 @@ let expand_root_path dir =
let rec aux = function
| [] -> []
| p :: l ->
- if p.path_root && is_dirpath_prefix_of p.path_logical dir then
- let suffix = drop_dirpath_prefix p.path_logical dir in
- extend_path_with_dirpath p.path_physical suffix :: aux l
+ if DirPath.equal p.path_logical dir then p.path_physical :: aux l
else aux l
in
aux !load_paths
-(* Root p is bound to A.B.C.D and we require file C.D.E.F *)
-(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *)
-
-(* Root p is bound to A.B.C.C and we require file C.C.E.F *)
-(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *)
-
-let intersections d1 d2 =
- let rec aux d1 =
- if DirPath.is_empty d1 then [d2] else
- let rest = aux (snd (chop_dirpath 1 d1)) in
- if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
- else rest in
- aux d1
-
-let expand p dir =
- let ph = extend_path_with_dirpath p.path_physical dir in
- let log = append_dirpath p.path_logical dir in
- (ph, log)
+let is_suffix dir1 dir2 =
+ let dir1 = DirPath.repr dir1 in
+ let dir2 = DirPath.repr dir2 in
+ List.prefix_of Id.equal dir1 dir2
let expand_path dir =
let rec aux = function
| [] -> []
| p :: l ->
- match p.path_implicit, p.path_root with
- | true, false -> expand p dir :: aux l
- | true, true ->
- let inters = intersections p.path_logical dir in
- List.map (expand p) inters @ aux l
- | false, true ->
- if is_dirpath_prefix_of p.path_logical dir then
- expand p (drop_dirpath_prefix p.path_logical dir) :: aux l
- else aux l
- | false, false ->
- (* nothing to do, an explicit root path should also match above
- if [is_dirpath_prefix_of p.path_logical dir] were true here *)
- aux l in
+ let { path_physical = ph; path_logical = lg } = p in
+ match p.path_implicit with
+ | true ->
+ (** The path is implicit, so that we only want match the logical suffix *)
+ if is_suffix dir lg then (ph, lg) :: aux l else aux l
+ | false ->
+ (** Otherwise we must match exactly *)
+ if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
+ in
aux !load_paths