X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=d0ecf9ba22d241851933a343fd6406a82cc390cb;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=21ed483ad157bc64de0abe11bdf4b100766d3908;hpb=faafe87ce2f7906abc4638cd8f69d1b82dece371;p=helm.git diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 21ed483ad..d0ecf9ba2 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -30,7 +30,6 @@ open Printf open Http_getter_common open Http_getter_misc -open Http_getter_debugger open Http_getter_types exception Not_implemented of string @@ -43,6 +42,10 @@ type resolve_result = | Exception of exn | Resolved of string +type logger_callback = HelmLogger.html_tag -> unit + +let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag) + let not_implemented s = raise (Not_implemented ("Http_getter." ^ s)) let (index_line_sep_RE, index_sep_RE, trailing_types_RE, @@ -64,10 +67,51 @@ let rdf_map = let xsl_map = lazy (new Http_getter_map.map (Lazy.force Http_getter_env.xsl_dbm)) +let uri_tree = ref None +let deref_if_some r = + match !r with + | None -> assert false + | Some x -> x +let is_prefetch_on () = + match !uri_tree with None -> false | Some _ -> true + +let dump_tree () = + let path = Lazy.force Http_getter_env.dump_file in + Tree.save_to_disk path (deref_if_some uri_tree); + Http_getter_md5.create_hash [ + (Lazy.force Http_getter_env.cic_dbm_real); + path ] + +let load_tree () = + if not (Http_getter_md5.check_hash ()) then + assert false + else + uri_tree := Some (Tree.load_from_disk + (Lazy.force Http_getter_env.dump_file)) + +let sync_with_map () = + if not (Http_getter_md5.check_hash ()) then begin + let tree = ref (Some Tree.empty_tree) in + Http_getter_logger.log "Updating cic map dump..."; + let t = Unix.time () in + (Lazy.force cic_map)#iter + (fun k _ -> + tree := Some (Tree.add_uri k (deref_if_some tree))); + uri_tree := !tree; + Http_getter_logger.log + (sprintf "done in %.0f sec" (Unix.time () -. t)); + dump_tree () + end else begin + Http_getter_logger.log "Cic map dump is up to date!"; + load_tree () (* XXX TASSI: race condition here *) + end + let maps = [ cic_map; nuprl_map; rdf_map; xsl_map ] let close_maps () = List.iter (fun m -> (Lazy.force m) # close) maps let clear_maps () = List.iter (fun m -> (Lazy.force m) # clear) maps -let sync_maps () = List.iter (fun m -> (Lazy.force m) # sync) maps +let sync_maps () = + List.iter (fun m -> (Lazy.force m) # sync) maps; + sync_with_map () let map_of_uri = function | uri when is_cic_uri uri -> Lazy.force cic_map @@ -76,8 +120,8 @@ let map_of_uri = function | uri when is_xsl_uri uri -> Lazy.force xsl_map | uri -> raise (Unresolvable_URI uri) -let update_from_server logmsg server_url = (* use global maps *) - debug_print ("Updating information from " ^ server_url); +let update_from_server logger server_url = (* use global maps *) + Http_getter_logger.log ("Updating information from " ^ server_url); let xml_url_of_uri = function (* TODO missing sanity checks on server_url, e.g. it can contains $1 *) | uri when (Pcre.pmatch ~rex:heading_cic_RE uri) -> @@ -95,7 +139,8 @@ let update_from_server logmsg server_url = (* use global maps *) Pcre.replace ~rex:heading_rdf_theory_RE ~templ:server_url uri | uri -> raise (Invalid_URI uri) in - let log = ref (`T ("Processing server: " ^ server_url) :: logmsg) in + logger (`T ("Processing server: " ^ server_url)); + logger `BR; let (xml_index, rdf_index, xsl_index) = (* TODO keeps index in memory, is better to keep them on temp files? *) (http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xml_index)), @@ -103,10 +148,11 @@ let update_from_server logmsg server_url = (* use global maps *) http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xsl_index))) in if (xml_index = None && rdf_index = None && xsl_index = None) then - debug_print (sprintf "Warning: useless server %s" server_url); + Http_getter_logger.log (sprintf "Warning: useless server %s" server_url); (match xml_index with | Some xml_index -> - (log := `T "Updating XML db ...
" :: !log; + logger (`T "- Updating XML db ..."); +(* logger `BR; *) List.iter (function | l when is_blank_line l -> () (* skip blank and commented lines *) @@ -121,15 +167,20 @@ let update_from_server logmsg server_url = (* use global maps *) assert (is_cic_uri uri || is_nuprl_uri uri) ; (map_of_uri uri)#replace uri ((xml_url_of_uri uri) ^ ".xml") - | _ -> log := `T ("Ignoring invalid line: '" ^ l) :: !log) + | _ -> + logger (`T ("Ignoring invalid line: '" ^ l)); + logger `BR) with Invalid_URI uri -> - log := `T ("Ignoring invalid XML URI: '" ^ l) :: !log)) + logger (`T ("Ignoring invalid XML URI: '" ^ l)); + logger `BR)) (Pcre.split ~rex:index_sep_RE xml_index); (* xml_index lines *) - log := `T "All done" :: !log) + logger (`T "All done"); + logger `BR | None -> ()); (match rdf_index with | Some rdf_index -> - (log := `T "Updating RDF db ..." :: !log; + logger (`T "- Updating RDF db ..."); +(* logger `BR; *) List.iter (fun l -> try @@ -140,38 +191,38 @@ let update_from_server logmsg server_url = (* use global maps *) | [uri] -> (Lazy.force rdf_map) # replace uri ((rdf_url_of_uri uri) ^ ".xml") - | _ -> log := `T ("Ignoring invalid line: '" ^ l) :: !log) + | _ -> + logger (`T ("Ignoring invalid line: '" ^ l)); + logger `BR) with Invalid_URI uri -> - log := `T ("Ignoring invalid RDF URI: '" ^ l) :: !log) + logger (`T ("Ignoring invalid RDF URI: '" ^ l)); + logger `BR) (Pcre.split ~rex:index_sep_RE rdf_index); (* rdf_index lines *) - log := `T "All done" :: !log) + logger (`T "All done"); + logger `BR | None -> ()); (match xsl_index with | Some xsl_index -> - (log := `T "Updating XSLT db ..." :: !log; + logger (`T "- Updating XSLT db ..."); +(* logger `BR; *) List.iter (fun l -> (Lazy.force xsl_map) # replace l (server_url ^ "/" ^ l)) (Pcre.split ~rex:index_sep_RE xsl_index); - log := `T "All done" :: !log) + logger (`T "All done"); + logger `BR | None -> ()); - debug_print "done with this server"; - !log + Http_getter_logger.log "done with this server" -let update_from_all_servers () = (* use global maps *) +let update_from_all_servers logger () = (* use global maps *) clear_maps (); - let log = - List.fold_left - update_from_server - [] (* initial logmsg: empty *) - (* reverse order: 1st server is the most important one *) - (List.map snd (List.rev (Http_getter_env.servers ()))) - in - sync_maps (); - `Msg (`L (List.rev log)) + List.iter + (update_from_server logger) + (* reverse order: 1st server is the most important one *) + (List.map snd (List.rev (Http_getter_env.servers ()))); + sync_maps () -let update_from_one_server server_url = - let log = update_from_server [] server_url in - `Msg (`L (List.rev log)) +let update_from_one_server ?(logger = fun _ -> ()) server_url = + update_from_server logger server_url let temp_file_of_uri uri = let flat_string s s' c = @@ -198,8 +249,10 @@ let getxslt_remote ~patch_dtd uri = not_implemented "getxslt_remote" let getdtd_remote ~patch_dtd uri = not_implemented "getdtd_remote" let clean_cache_remote () = not_implemented "clean_cache_remote" let list_servers_remote () = not_implemented "list_servers_remote" -let add_server_remote ~position name = not_implemented "add_server_remote" -let remove_server_remote position = not_implemented "remove_server_remote" +let add_server_remote ~logger ~position name = + not_implemented "add_server_remote" +let remove_server_remote ~logger position = + not_implemented "remove_server_remote" let getalluris_remote () = not_implemented "getalluris_remote" let getallrdfuris_remote () = not_implemented "getallrdfuris_remote" let ls_remote lsuri = not_implemented "ls_remote" @@ -209,14 +262,17 @@ let resolve_remote uri = (* deliver resolve request to http_getter *) let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in let res = ref Unknown in - Pxp_yacc.process_entity Pxp_yacc.default_config (`Entry_content []) - (Pxp_yacc.create_entity_manager ~is_document:true Pxp_yacc.default_config - (Pxp_yacc.from_string doc)) + Pxp_ev_parser.process_entity PxpHelmConf.pxp_config (`Entry_content []) + (Pxp_ev_parser.create_entity_manager ~is_document:true + PxpHelmConf.pxp_config (Pxp_yacc.from_string doc)) (function - | Pxp_yacc.E_start_tag ("url",["value",url],_) -> res := Resolved url - | Pxp_yacc.E_start_tag ("unresolved",[],_) -> + | Pxp_types.E_start_tag ("url",["value",url],_,_) -> res := Resolved url + | Pxp_types.E_start_tag ("unresolvable",[],_,_) -> res := Exception (Unresolvable_URI uri) - | Pxp_yacc.E_start_tag _ -> res := Exception UnexpectedGetterOutput + | Pxp_types.E_start_tag ("not_found",[],_,_) -> + res := Exception (Key_not_found uri) + | Pxp_types.E_start_tag (x,_,_,_) -> + res := Exception UnexpectedGetterOutput | _ -> ()); match !res with | Unknown -> raise UnexpectedGetterOutput @@ -226,19 +282,22 @@ let resolve_remote uri = let register_remote ~uri ~url = ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) -let register_remote ~uri ~url = - ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) +let unregister_remote uri = + ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri) -let update_remote () = +let update_remote logger () = let answer = ClientHTTP.get (getter_url () ^ "update") in - `Msg (`T answer) + logger (`T answer); + logger `BR let getxml_remote ~format ~patch_dtd uri = - ClientHTTP.get_and_save_to_tmp - (sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s" - (getter_url ()) uri - (match format with Enc_normal -> "normal" | Enc_gzipped -> "gzipped") - (match patch_dtd with true -> "yes" | false -> "no")) + let uri = + sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s" + (getter_url ()) uri + (match format with `Normal -> "normal" | `Gzipped -> "gz") + (match patch_dtd with true -> "yes" | false -> "no") + in + ClientHTTP.get_and_save_to_tmp uri (* API *) @@ -248,31 +307,46 @@ let resolve uri = if remote () then resolve_remote uri else - try - (map_of_uri uri)#resolve uri - with Http_getter_map.Key_not_found _ -> raise (Unresolvable_URI uri) - - (* Warning: this fail if uri is already registered *) + (map_of_uri uri)#resolve uri + let register ~uri ~url = if remote () then register_remote ~uri ~url else - (map_of_uri uri)#add uri url + begin + (map_of_uri uri)#add uri url; + if is_prefetch_on () then + uri_tree := Some (Tree.add_uri uri (deref_if_some uri_tree)) + end -let update () = +let unregister uri = if remote () then - update_remote () + unregister_remote uri else - update_from_all_servers () + try + begin + (map_of_uri uri)#remove uri; + if is_prefetch_on () then + uri_tree := Some (Tree.remove_uri uri (deref_if_some uri_tree)) + end + with Key_not_found _ -> () + +let update ?(logger = fun _ -> ()) () = + if remote () then + update_remote logger () + else + update_from_all_servers logger () -let getxml ?(format = Enc_normal) ?(patch_dtd = true) uri = +let getxml ?(format = `Gzipped) ?(patch_dtd = false) uri = if remote () then getxml_remote ~format ~patch_dtd uri else begin + Http_getter_logger.log ~level:2 ("getxml: " ^ uri); let url = resolve uri in + Http_getter_logger.log ~level:2 ("resolved_uri: " ^ url) ; let (fname, outchan) = temp_file_of_uri uri in - Http_getter_cache.respond_xml ~uri ~url ~enc:format ~patch:patch_dtd - outchan; + Http_getter_cache.respond_xml ~via_http:false ~enc:format ~patch:patch_dtd + ~uri ~url outchan; close_out outchan; fname end @@ -281,9 +355,10 @@ let getxslt ?(patch_dtd = true) uri = if remote () then getxslt_remote ~patch_dtd uri else begin + let url = resolve uri in let (fname, outchan) = temp_file_of_uri uri in - Http_getter_cache.respond_xsl ~url ~patch:patch_dtd outchan; + Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan; close_out outchan; fname end @@ -294,7 +369,7 @@ let getdtd ?(patch_dtd = true) uri = else begin let url = Lazy.force Http_getter_env.dtd_dir ^ "/" ^ uri in let (fname, outchan) = temp_file_of_uri uri in - Http_getter_cache.respond_dtd ~url ~patch:patch_dtd outchan; + Http_getter_cache.respond_dtd ~via_http:false ~url ~patch:patch_dtd outchan; close_out outchan; fname end @@ -311,23 +386,25 @@ let list_servers () = else Http_getter_env.servers () -let add_server ?(position = 0) name = +let add_server ?(logger = fun _ -> ()) ?(position = 0) name = if remote () then - add_server_remote ~position name + add_server_remote ~logger ~position name else begin if position = 0 then begin Http_getter_env.add_server ~position:0 name; - update_from_one_server name (* quick update (new server only) *) + update_from_one_server ~logger name (* quick update (new server only) *) end else if position > 0 then begin Http_getter_env.add_server ~position name; - update () - end else (* already checked bt parse_position *) + update ~logger () + end else (* already checked by parse_position *) assert false end -let remove_server position = +let has_server position = List.mem_assoc position (Http_getter_env.servers ()) + +let remove_server ?(logger = fun _ -> ()) position = if remote () then - remove_server_remote () + remove_server_remote ~logger () else begin let server_name = try @@ -336,7 +413,7 @@ let remove_server position = raise (Invalid_argument (sprintf "no server with position %d" position)) in Http_getter_env.remove_server position; - update () + update ~logger () end let return_uris map filter = @@ -349,8 +426,8 @@ let getalluris () = getalluris_remote () else let filter uri = - (Pcre.pmatch ~rex:heading_cic_RE uri) && - not (Pcre.pmatch ~rex:trailing_types_RE uri) + (Pcre.pmatch ~rex:heading_cic_RE uri) +(* && not (Pcre.pmatch ~rex:trailing_types_RE uri) *) in return_uris (Lazy.force cic_map) filter @@ -366,93 +443,219 @@ let getallrdfuris classs = in return_uris (Lazy.force rdf_map) filter -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) = - (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 "^[^/]*$") - in - fun lsuri -> - if remote () then - ls_remote lsuri - else begin - let pat = - "^" ^ - (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p)) - in - let (dir_RE, obj_RE) = - (Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "(\\.|$)")) + +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" 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 + try + ignore (resolve theory); + true + with Key_not_found _ -> false + 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 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 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 - (Lazy.force cic_map) # iter - (* BLEARGH Dbm module lacks support for fold-like functions *) - (fun key _ -> - match key with - | uri when Pcre.pmatch ~rex:dir_RE uri -> (* directory hit *) - let localpart = Pcre.replace ~rex:dir_RE uri in - if Pcre.pmatch ~rex:no_slashes_RE localpart then - store_obj localpart + Hashtbl.replace objs basepart (oldflags ++ newflags) + in + (* Variables used in backward compatibility code to map + theory:/path/t.theory into theory:/path/t/index.theory + when cic:/path/t/ exists *) + let the_candidate_for_remapping = + (* CSC: Here I am making a strong assumption: the pattern + can be only of the form [^:]*:/path where path is + NOT a regular expression *) + "theory:" ^ Pcre.replace ~rex:(Pcre.regexp "[^:]*:") pat + in + let index_not_generated_yet = ref true in + let valid_candidates = ref [] in + let candidates_found = ref [] in + + (*(Lazy.force cic_map) # iter*) + + (* depending on prefetch *) + let if_prefetch if_is if_not = + if is_prefetch_on() then if_is else if_not + in + + let iter_on_right_thing = if_prefetch + (fun f -> List.iter (fun k -> f k "") + (Tree.ls_path regexp (deref_if_some uri_tree))) + (fun f -> (Lazy.force cic_map) # iter f) + in + let calculate_localpart = if_prefetch + (fun uri -> uri) + (fun uri -> Pcre.replace ~rex:dir_RE uri) + in + let check_if_x_RE = if_prefetch + (fun x_RE uri -> true) + (fun x_RE uri -> Pcre.pmatch ~rex:x_RE uri) + in + let check_if_dir_RE = check_if_x_RE dir_RE in + let check_if_obj_RE = check_if_x_RE obj_RE in + + iter_on_right_thing + (fun key _ -> + (* we work in two ways: + * 1 iteration on the whole map + * 2 tree visit + * + * Since in the first case 'key' is a complete uri, while + * in the second case it is only the subtree rooted in the + * query regex, we must relay only on the localpath. + * + * example: + * query::= cic:/aaa/bbb/ + * + * answer1 ::= the whole map + * + * aswer2 ::= [ "ccc/"; "c1.something"] where + * cic:/aaa/bbb/ccc/ and cic:/aaa/bbb/c1.something + * are the (partials) uri that matched query + * + * after the localpath extracion we have more uris in the first case, + * but at least the are all rooted in the same node. + * + * the Tree.get_frontier may be changed to return the same stuff as + * the map iteration+localpath extraction does, but I hope it is not + * necessary + *) + match key with + | uri when looking_for_dir && check_if_dir_RE uri -> + (* directory hit *) + let localpart = calculate_localpart uri in + if Pcre.pmatch ~rex:no_slashes_RE localpart then + begin + (* Backward compatibility code to map + theory:/path/t.theory into theory:/path/t/index.theory + when cic:/path/t/ exists *) + if Pcre.pmatch ~rex:theory_RE localpart then + candidates_found := localpart :: !candidates_found else - store_dir localpart - | uri when Pcre.pmatch ~rex:obj_RE uri -> (* file hit *) - store_obj (Pcre.replace ~rex:til_slash_RE uri) - | uri -> () (* miss *)); - let ls_items = ref [] in - StringSet.iter (fun dir -> ls_items := Ls_section dir :: !ls_items) !dirs; - Http_getter_misc.hashtbl_sorted_iter - (fun uri (annflag, typesflag, bodyflag, treeflag) -> - ls_items := - Ls_object { - uri = uri; ann = annflag; - types = typesflag; body = bodyflag; proof_tree = treeflag - } :: !ls_items) - objs; - List.rev !ls_items - end + store_obj localpart + end + else + begin + store_dir localpart ; + if Pcre.pmatch localpart ~rex:dir_local_RE then + begin + let valid = + Pcre.replace ~rex:first_comp_RE localpart ^ ".theory" + in + if not (List.mem valid !valid_candidates) then + valid_candidates := valid::!valid_candidates + end + end + | uri when (not looking_for_dir) && check_if_obj_RE uri -> + (* file hit *) + store_obj (Pcre.replace ~rex:til_slash_RE uri) + | uri -> ()); +(* + (* miss *) + if !index_not_generated_yet && + Pcre.pmatch ~rex:orig_theory_RE uri + then + (index_not_generated_yet := false ; + store_obj "index.theory")); + *) + if exists_theory regexp then store_obj "index.theory"; + List.iter + (fun localpart -> + if not (List.mem localpart !valid_candidates) then + store_obj localpart + ) !candidates_found ; + let ls_items = ref [] in + StringSet.iter (fun dir -> ls_items := Ls_section dir :: !ls_items) !dirs; + Http_getter_misc.hashtbl_sorted_iter + (fun uri (annflag, typesflag, bodyflag, treeflag) -> + ls_items := + Ls_object { + uri = uri; ann = annflag; + types = typesflag; body = bodyflag; proof_tree = treeflag + } :: !ls_items) + objs; + List.rev !ls_items + end - (* Shorthands from now on *) +(* Shorthands from now on *) let getxml' uri = getxml (UriManager.string_of_uri uri) let resolve' uri = resolve (UriManager.string_of_uri uri) let register' uri url = register ~uri:(UriManager.string_of_uri uri) ~url +let unregister' uri = unregister (UriManager.string_of_uri uri) + +let sync_dump_file () = + if is_prefetch_on () then + dump_tree () + +let init () = + Http_getter_logger.set_log_level + (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level"); + Http_getter_logger.set_log_file + (Helm_registry.get_opt Helm_registry.get_string "getter.log_file"); + Http_getter_env.reload (); + let is_prefetch_set = + Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch" + in + if is_prefetch_set then + (* ignore (Thread.create sync_with_map ()) *) + sync_with_map ()