X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=ec6564249270e627d40facb4a9af47c9670bfa95;hb=f0196d4e96bf8cc579d1690fc6a653adc08ca02e;hp=501b9d8390dd8692488a0d095ed87adeffd92077;hpb=b93fd4b7d0835fd5b35ad5615f6b8b105a827280;p=helm.git
diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index 501b9d839..ec6564249 100644
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -71,16 +71,21 @@ let parse_output_format (req: Http_types.request) =
let parse_ls_uri =
let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in
let trailing_slash_RE = Pcre.regexp "/+$" in
+ let wrong_uri uri =
+ raise (Http_getter_bad_request ("Invalid /ls baseuri: " ^ uri))
+ in
fun (req: Http_types.request) ->
let baseuri = req#param "baseuri" in
- let subs =
- Pcre.extract ~rex:parse_ls_RE
- (Pcre.replace ~rex:trailing_slash_RE baseuri)
- in
- match (subs.(1), subs.(2)) with
- | "cic", uri -> Cic uri
- | "theory", uri -> Theory uri
- | _ -> raise (Http_getter_bad_request ("Invalid /ls baseuri: " ^ baseuri))
+ try
+ let subs =
+ Pcre.extract ~rex:parse_ls_RE
+ (Pcre.replace ~rex:trailing_slash_RE baseuri)
+ in
+ (match (subs.(1), subs.(2)) with
+ | "cic", uri -> Cic uri
+ | "theory", uri -> Theory uri
+ | _ -> wrong_uri baseuri)
+ with Not_found -> wrong_uri baseuri
;;
(* global maps, shared by all threads *)
@@ -90,8 +95,11 @@ let nuprl_map = new Http_getter_map.map Http_getter_env.nuprl_dbm in
let rdf_map = new Http_getter_map.map Http_getter_env.rdf_dbm in
let xsl_map = new Http_getter_map.map Http_getter_env.xsl_dbm in
-let save_maps () =
- cic_map#close; nuprl_map#close; rdf_map#close; xsl_map#close in
+let maps = [ cic_map; nuprl_map; rdf_map; xsl_map ] in
+let close_maps () = List.iter (fun m -> m#close) maps in
+let clear_maps () = List.iter (fun m -> m#clear) maps in
+let sync_maps () = List.iter (fun m -> m#sync) maps in
+
let map_of_uri = function
| uri when is_cic_uri uri -> cic_map
| uri when is_nuprl_uri uri -> nuprl_map
@@ -138,17 +146,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 "^[^/]*$")
@@ -168,18 +181,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
@@ -202,10 +219,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
@@ -229,17 +248,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
@@ -332,7 +353,7 @@ let update_from_server logmsg server_url = (* use global maps *)
!log
in
let update_from_all_servers () = (* use global maps *)
- cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear;
+ clear_maps ();
let log =
List.fold_left
update_from_server
@@ -340,7 +361,7 @@ let update_from_all_servers () = (* use global maps *)
(* reverse order: 1st server is the most important one *)
(List.rev !Http_getter_env.servers)
in
- cic_map#sync; nuprl_map#sync; rdf_map#sync; xsl_map#sync;
+ sync_maps ();
log
in
@@ -382,6 +403,9 @@ let callback (req: Http_types.request) outchan =
register uri url;
return_html_msg "Register done" outchan
| _ -> assert false)
+ | "/clean_cache" ->
+ Http_getter_cache.clean ();
+ return_html_msg "Done." outchan
| "/update" ->
Http_getter_env.reload (); (* reload servers list from servers file *)
let log = update_from_all_servers () in
@@ -502,12 +526,12 @@ let main () =
print_string (Http_getter_env.env_to_string ());
flush stdout;
Unix.putenv "http_proxy" "";
- at_exit save_maps;
+ at_exit close_maps;
Sys.catch_break true;
try
Http_daemon.start'
~timeout:(Some 600) ~port:Http_getter_env.port ~mode:`Thread callback
- with Sys.Break -> () (* 'save_maps' already registered with 'at_exit' *)
+ with Sys.Break -> () (* 'close_maps' already registered with 'at_exit' *)
in
main ()