X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=ac8b98305b2c392450da5fe3629a9c6d30284f2e;hb=b2c29f8bef99b45f71bc0c5ee656304094d16113;hp=48c82f8eaae356ba2f7f5218c35600b4dc1720b0;hpb=d838a20f709408384d53cb0377891b89d2a76f94;p=helm.git
diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index 48c82f8ea..ac8b98305 100644
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -143,17 +143,22 @@ in
let return_all_xml_uris = return_all_foo_uris cic_map "alluris" in
let return_all_rdf_uris = return_all_foo_uris rdf_map "allrdfuris" in
let return_ls =
- let (++) (oldann, oldtypes, oldbody) (newann, newtypes, newbody) =
+ 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 newbody > oldbody then newbody else oldbody),
+ (if newtree > oldtree then newtree else oldtree))
in
let basepart_RE =
- Pcre.regexp "^([^.]*\\.[^.]*)((\\.body)|(\\.types))?(\\.ann)?"
+ Pcre.regexp
+ "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?"
in
- let (types_RE, types_ann_RE, body_RE, body_ann_RE) =
- (Pcre.regexp "\\.types", Pcre.regexp "\\.types.ann",
- Pcre.regexp "\\.body", Pcre.regexp "\\.body.ann")
+ let (types_RE, types_ann_RE, body_RE, body_ann_RE,
+ proof_tree_RE, proof_tree_ann_RE) =
+ (Pcre.regexp "\\.types", Pcre.regexp "\\.types\\.ann",
+ Pcre.regexp "\\.body", Pcre.regexp "\\.body.ann",
+ Pcre.regexp "\\.proof_tree", Pcre.regexp "\\.proof_tree\\.ann")
in
let (slash_RE, til_slash_RE, no_slashes_RE) =
(Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
@@ -173,18 +178,22 @@ let return_ls =
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 -> (false, No, No) (* no ann, no types, no body *)
+ 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)
- | s when Pcre.pmatch ~rex:types_ann_RE s -> (true, Ann, No)
- | s when Pcre.pmatch ~rex:body_RE s -> (false, No, Yes)
- | s when Pcre.pmatch ~rex:body_ann_RE s -> (true, No, Ann)
- | s -> (false, No, No)
+ | 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)
in
@@ -207,10 +216,12 @@ let return_ls =
(fun s d -> sprintf "%sdir, %s\n" s d) ""
(StringSet.elements !dirs)) ^
(Http_getter_misc.hashtbl_sorted_fold
- (fun uri (annflag, typesflag, bodyflag) cont ->
- sprintf "%sobject, %s, <%s,%s,%s>\n"
+ (fun uri (annflag, typesflag, bodyflag, treeflag) cont ->
+ sprintf "%sobject, %s, <%s,%s,%s,%s>\n"
cont uri (if annflag then "YES" else "NO")
- (string_of_ls_flag typesflag) (string_of_ls_flag bodyflag))
+ (string_of_ls_flag typesflag)
+ (string_of_ls_flag bodyflag)
+ (string_of_ls_flag treeflag))
objs "")
in
Http_daemon.respond
@@ -234,17 +245,19 @@ let return_ls =
(fun d -> "" ^ d ^ "")
(StringSet.elements !dirs))) ^ "\n" ^
(Http_getter_misc.hashtbl_sorted_fold
- (fun uri (annflag, typesflag, bodyflag) cont ->
+ (fun uri (annflag, typesflag, bodyflag, treeflag) cont ->
sprintf
"%s
+\t
"
cont uri (if annflag then "YES" else "NO")
(string_of_ls_flag typesflag)
- (string_of_ls_flag bodyflag))
+ (string_of_ls_flag bodyflag)
+ (string_of_ls_flag treeflag))
objs ""))
in
Http_daemon.respond