-let ls =
- let (++) (oldann, oldtypes, oldbody, oldtree)
- (newann, newtypes, newbody, newtree) =
- ((if newann > oldann then newann else oldann),
- (if newtypes > oldtypes then newtypes else oldtypes),
- (if newbody > oldbody then newbody else oldbody),
- (if newtree > oldtree then newtree else oldtree))
- in
- let basepart_RE =
- Pcre.regexp
- "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
- in
- let (types_RE, types_ann_RE, body_RE, body_ann_RE,
- proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE, theory_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 "/$", Pcre.regexp "\\.theory$")
- in
- let (slash_RE, til_slash_RE, no_slashes_RE) =
- (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
- in
- fun regexp ->
- if remote () then
- ls_remote regexp
- else begin
- 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, dir_RE2, obj_RE, orig_theory_RE) =
- Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "/[^/]*"),
- Pcre.regexp (pat ^ "(\\.|$)"), Pcre.regexp (pat ^ ".theory$")
- in
- let dirs = ref StringSet.empty in
- let objs = Hashtbl.create 17 in
- let store_dir d =
- dirs := StringSet.add (List.hd (Pcre.split ~rex:slash_RE d)) !dirs
- in
- let store_obj o =
- let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
- let no_flags = false, No, No, No in
- let oldflags =
- try
- Hashtbl.find objs basepart
- with Not_found -> (* no ann, no types, no body, no proof tree *)
- no_flags
- in
- let newflags =
- match o with
- | s when Pcre.pmatch ~rex:types_RE s -> (false, Yes, No, No)
- | s when Pcre.pmatch ~rex:types_ann_RE s -> (true, Ann, No, No)
- | s when Pcre.pmatch ~rex:body_RE s -> (false, No, Yes, No)
- | s when Pcre.pmatch ~rex:body_ann_RE s -> (true, No, Ann, No)
- | s when Pcre.pmatch ~rex:proof_tree_RE s -> (false, No, No, Yes)
- | s when Pcre.pmatch ~rex:proof_tree_ann_RE s -> (true, No, No, Ann)
- | s -> no_flags
- in
- Hashtbl.replace objs basepart (oldflags ++ newflags)
+
+let (++) (oldann, oldtypes, oldbody, oldtree)
+ (newann, newtypes, newbody, newtree) =
+ ((if newann > oldann then newann else oldann),
+ (if newtypes > oldtypes then newtypes else oldtypes),
+ (if newbody > oldbody then newbody else oldbody),
+ (if newtree > oldtree then newtree else oldtree))
+
+let (types_RE, types_ann_RE, body_RE, body_ann_RE,
+ proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE, theory_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 "/$", Pcre.regexp "\\.theory$")
+
+let basepart_RE =
+ Pcre.regexp
+ "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
+
+let (slash_RE, til_slash_RE, no_slashes_RE) =
+ (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
+
+let ls regexp =
+ if remote () then
+ ls_remote regexp
+ else begin
+ 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, dir_local_RE, obj_RE, first_comp_RE) =
+ Pcre.regexp (pat ^ "/"), Pcre.regexp "[^/]+/[^/]*",
+ Pcre.regexp (pat ^ "(\\.|$)"), Pcre.regexp "/.*"
+ in
+ let toplevel_theory =
+ match List.rev (Pcre.split ~rex:slash_RE pat) with
+ | dir :: _ -> Some (dir ^ ".theory")
+ | _ -> None
+ in
+ let dirs = ref StringSet.empty in
+ let objs = Hashtbl.create 17 in
+ let store_dir d =
+ dirs := StringSet.add (List.hd (Pcre.split ~rex:slash_RE d)) !dirs
+ in
+ let store_obj o =
+ let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
+ let no_flags = false, No, No, No in
+ let oldflags =
+ try
+ Hashtbl.find objs basepart
+ with Not_found -> (* no ann, no types, no body, no proof tree *)
+ no_flags