diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-31 18:25:45 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-31 18:36:21 +0200 |
commit | 765510929b2255d9c56fcdfce4a3ea555b07b340 (patch) | |
tree | 368fda2d2a4fde7b3f70f6ad8bae6442a8001f07 /library/loadpath.ml | |
parent | e52303164660041690f6e05a110ff633007a1dd5 (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.ml | 48 |
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 |