"^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
in
let (types_RE, types_ann_RE, body_RE, body_ann_RE,
- proof_tree_RE, proof_tree_ann_RE) =
+ proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE) =
(Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
- Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$")
+ Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$",
+ Pcre.regexp "/$")
in
let (slash_RE, til_slash_RE, no_slashes_RE) =
(Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
in
- fun lsuri ->
+ fun regexp ->
if remote () then
- ls_remote lsuri
+ ls_remote regexp
else begin
- let pat =
- "^" ^
- (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p))
- in
+ let looking_for_dir = Pcre.pmatch ~rex:trailing_slash_RE regexp in
+ let pat = Pcre.replace ~rex:trailing_slash_RE ("^" ^ regexp) in
let (dir_RE, obj_RE) =
(Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "(\\.|$)"))
in
(* BLEARGH Dbm module lacks support for fold-like functions *)
(fun key _ ->
match key with
- | uri when Pcre.pmatch ~rex:dir_RE uri -> (* directory hit *)
+ | uri when looking_for_dir && Pcre.pmatch ~rex:dir_RE uri ->
+ (* directory hit *)
let localpart = Pcre.replace ~rex:dir_RE uri in
if Pcre.pmatch ~rex:no_slashes_RE localpart then
store_obj localpart
else
store_dir localpart
- | uri when Pcre.pmatch ~rex:obj_RE uri -> (* file hit *)
+ | uri when (not looking_for_dir) && Pcre.pmatch ~rex:obj_RE uri ->
+ (* file hit *)
store_obj (Pcre.replace ~rex:til_slash_RE uri)
| uri -> () (* miss *));
let ls_items = ref [] in