-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
+
+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 fix_regexp_RE = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
+
+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 exists_theory regexp =
+ let theory =
+ Pcre.replace ~rex:fix_regexp_RE ~templ:"theory" regexp ^ "index.theory"