X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=ec6564249270e627d40facb4a9af47c9670bfa95;hb=970ba0021a992efe25ec374875dc127ff236cc74;hp=d8526afa99d61f453a1087d08020b9c7260b5ba0;hpb=a4520a0d408ece8a4e3cc1dab3f89e91f01f623d;p=helm.git diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index d8526afa9..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 \t \t +\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,10 +403,22 @@ 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 return_html_msg log outchan + | "/list_servers" -> + return_html_raw + (sprintf "\n%s\n
" + (String.concat "\n" + (List.map + (let i = ref ~-1 in + fun s -> incr i; sprintf "%d%s" !i s) + !Http_getter_env.servers))) + outchan | "/add_server" -> let name = req#param "url" in (try @@ -493,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 ()