X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=f7ca2388c89b9653d04f8087ac4d021fc8d1e966;hb=b41886e9d21d756279bd6a2ec3f19c17b1a64401;hp=a817f7448d52a6baa35241bb91246c41f9b71bfb;hpb=f44ab01307f10d4165c76e3108542a5bc2035766;p=helm.git diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index a817f7448..f7ca2388c 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 @@ -45,6 +44,8 @@ type resolve_result = 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, @@ -79,7 +80,7 @@ let map_of_uri = function | uri -> raise (Unresolvable_URI uri) let update_from_server logger server_url = (* use global maps *) - debug_print ("Updating information from " ^ server_url); + 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) -> @@ -106,11 +107,11 @@ let update_from_server logger 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 -> - logger (`T "Updating XML db ..."); - logger `BR; + logger (`T "- Updating XML db ..."); +(* logger `BR; *) List.iter (function | l when is_blank_line l -> () (* skip blank and commented lines *) @@ -137,8 +138,8 @@ let update_from_server logger server_url = (* use global maps *) | None -> ()); (match rdf_index with | Some rdf_index -> - logger (`T "Updating RDF db ..."); - logger `BR; + logger (`T "- Updating RDF db ..."); +(* logger `BR; *) List.iter (fun l -> try @@ -161,15 +162,15 @@ let update_from_server logger server_url = (* use global maps *) | None -> ()); (match xsl_index with | Some xsl_index -> - logger (`T "Updating XSLT db ..."); - logger `BR; + 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); logger (`T "All done"); logger `BR | None -> ()); - debug_print "done with this server" + Http_getter_logger.log "done with this server" let update_from_all_servers logger () = (* use global maps *) clear_maps (); @@ -207,8 +208,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 ~logger ~position name = not_implemented "add_server_remote" -let remove_server_remote ~logger 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" @@ -218,14 +221,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 @@ -235,12 +241,13 @@ 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 logger () = let answer = ClientHTTP.get (getter_url () ^ "update") in - logger (`T answer) + logger (`T answer); + logger `BR let getxml_remote ~format ~patch_dtd uri = ClientHTTP.get_and_save_to_tmp @@ -257,17 +264,22 @@ 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 +let unregister uri = + if remote () then + unregister_remote uri + else + try + (map_of_uri uri)#remove uri + with Key_not_found _ -> () + let update ?(logger = fun _ -> ()) () = if remote () then update_remote logger () @@ -278,7 +290,9 @@ let getxml ?(format = `Normal) ?(patch_dtd = true) 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 ~via_http:false ~enc:format ~patch:patch_dtd ~uri ~url outchan; @@ -290,6 +304,7 @@ 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 ~via_http:false ~url ~patch:patch_dtd outchan; @@ -360,8 +375,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 @@ -390,24 +405,24 @@ let ls = "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$" in let (types_RE, types_ann_RE, body_RE, body_ann_RE, - proof_tree_RE, proof_tree_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 "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$", + Pcre.regexp "/$", Pcre.regexp "\\.theory$") in let (slash_RE, til_slash_RE, no_slashes_RE) = (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$") in - fun lsuri -> + fun regexp -> if remote () then - ls_remote lsuri + ls_remote regexp 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 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_RE2, obj_RE, orig_theory_RE) = + Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "/[^/]*"), + Pcre.regexp (pat ^ "(\\.|$)"), Pcre.regexp (pat ^ ".theory$") in let dirs = ref StringSet.empty in let objs = Hashtbl.create 17 in @@ -435,19 +450,64 @@ let ls = in 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 (* BLEARGH Dbm module lacks support for fold-like functions *) (fun key _ -> match key with - | uri when Pcre.pmatch ~rex:dir_RE uri -> (* directory hit *) + | uri when looking_for_dir && 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 + 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 := (uri,localpart) :: !candidates_found + else + store_obj localpart + + end else - store_dir localpart - | uri when Pcre.pmatch ~rex:obj_RE uri -> (* file hit *) + begin + store_dir localpart ; + if String.sub uri 0 3 = "cic" then + let dir_found = ref "" in + let _ = + Pcre.substitute_first ~rex:dir_RE2 + ~subst:(fun s -> dir_found := s; "") uri in + let dir = + "theory" ^ String.sub !dir_found 3 + (String.length !dir_found - 3) ^ ".theory" in + if not (List.mem dir !valid_candidates) then + valid_candidates := dir::!valid_candidates + end + | uri when (not looking_for_dir) && Pcre.pmatch ~rex:obj_RE uri -> + (* file hit *) store_obj (Pcre.replace ~rex:til_slash_RE uri) - | uri -> () (* miss *)); + | uri -> (* miss *) + if !index_not_generated_yet && + Pcre.pmatch ~rex:orig_theory_RE uri + then + (index_not_generated_yet := false ; + store_obj "index.theory")); + List.iter + (fun (uri,localpart) -> + if not (List.mem uri !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 @@ -466,4 +526,10 @@ let ls = 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 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 ()