X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=4094a7376268eb6a31036a874643e258cbad4e9a;hb=b6101c89b49ad1df07df62ec661c8b30bda99a2a;hp=4f80006c6d80ebda60a6223b863c9d24a338baa7;hpb=1d15266bc05ac3524d721b66933db9a49e4c24aa;p=helm.git diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 4f80006c6..4094a7376 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -35,8 +35,6 @@ open Http_getter_types exception Not_implemented of string exception UnexpectedGetterOutput -(* resolve_result is needed because it is not possible to raise *) -(* an exception in a pxp ever-processing callback. Too bad. *) type resolve_result = | Unknown | Exception of exn @@ -44,17 +42,18 @@ type resolve_result = type logger_callback = HelmLogger.html_tag -> unit -let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag) +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, - heading_cic_RE, heading_theory_RE, heading_nuprl_RE, - heading_rdf_cic_RE, heading_rdf_theory_RE) = - (Pcre.regexp "[ \t]+", Pcre.regexp "\r\n|\r|\n", - Pcre.regexp "\\.types$", - Pcre.regexp "^cic:", Pcre.regexp "^theory:", Pcre.regexp "^nuprl:", - Pcre.regexp "^helm:rdf.*//cic:", Pcre.regexp "^helm:rdf.*//theory:") +let index_line_sep_RE = Pcre.regexp "[ \t]+" +let index_sep_RE = Pcre.regexp "\r\n|\r|\n" +let trailing_types_RE = Pcre.regexp "\\.types$" +let heading_cic_RE = Pcre.regexp "^cic:" +let heading_theory_RE = Pcre.regexp "^theory:" +let heading_nuprl_RE = Pcre.regexp "^nuprl:" +let heading_rdf_cic_RE = Pcre.regexp "^helm:rdf.*//cic:" +let heading_rdf_theory_RE = Pcre.regexp "^helm:rdf.*//theory:" (* global maps, shared by all threads *) @@ -260,42 +259,52 @@ let ls_remote lsuri = not_implemented "ls_remote" let resolve_remote uri = (* deliver resolve request to http_getter *) - let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in + let doc = + Http_getter_wget.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) + in let res = ref Unknown in - 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_types.E_start_tag ("url",["value",url],_,_) -> res := Resolved url - | Pxp_types.E_start_tag ("unresolvable",[],_,_) -> - res := Exception (Unresolvable_URI uri) - | 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 - | Exception e -> raise e - | Resolved url -> url + let start_element tag attrs = + match tag with + | "url" -> + (try + res := Resolved (List.assoc "value" attrs) + with Not_found -> ()) + | "unresolvable" -> res := Exception (Unresolvable_URI uri) + | "not_found" -> res := Exception (Key_not_found uri) + | _ -> () + in + let callbacks = { + XmlPushParser.default_callbacks with + XmlPushParser.start_element = Some start_element + } in + let xml_parser = XmlPushParser.create_parser callbacks in + XmlPushParser.parse xml_parser (`String doc); + XmlPushParser.final xml_parser; + match !res with + | Unknown -> raise UnexpectedGetterOutput + | Exception e -> raise e + | Resolved url -> url let register_remote ~uri ~url = - ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) + Http_getter_wget.send + (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url) let unregister_remote uri = - ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri) + Http_getter_wget.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri) let update_remote logger () = - let answer = ClientHTTP.get (getter_url () ^ "update") in + let answer = Http_getter_wget.get (getter_url () ^ "update") in 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" + let uri = + sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s" (getter_url ()) uri - (match format with `Normal -> "normal" | `Gzipped -> "gzipped") - (match patch_dtd with true -> "yes" | false -> "no")) + (match format with `Normal -> "normal" | `Gzipped -> "gz") + (match patch_dtd with true -> "yes" | false -> "no") + in + Http_getter_wget.get_and_save_to_tmp uri (* API *) @@ -335,7 +344,7 @@ let update ?(logger = fun _ -> ()) () = else update_from_all_servers logger () -let getxml ?(format = `Normal) ?(patch_dtd = true) uri = +let getxml ?(format = `Gzipped) ?(patch_dtd = false) uri = if remote () then getxml_remote ~format ~patch_dtd uri else begin @@ -462,6 +471,7 @@ let basepart_RE = 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 @@ -473,6 +483,15 @@ let ls regexp = 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 + 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") @@ -604,7 +623,7 @@ let ls regexp = (index_not_generated_yet := false ; store_obj "index.theory")); *) - 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 @@ -636,13 +655,16 @@ let sync_dump_file () = let init () = Http_getter_logger.set_log_level - (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level"); + (Helm_registry.get_opt_default Helm_registry.int ~default:1 + "getter.log_level"); Http_getter_logger.set_log_file - (Helm_registry.get_opt Helm_registry.get_string "getter.log_file"); + (Helm_registry.get_opt Helm_registry.string "getter.log_file"); Http_getter_env.reload (); let is_prefetch_set = - Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch" + Helm_registry.get_opt_default Helm_registry.bool ~default:false + "getter.prefetch" in if is_prefetch_set then - ignore (Thread.create sync_with_map ()) + (* ignore (Thread.create sync_with_map ()) *) + sync_with_map ()