open Http_getter_common
open Http_getter_misc
-open Http_getter_debugger
open Http_getter_types
exception Not_implemented of string
| 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,
| 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) ->
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)),
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 ...<br />" :: !log;
+ logger (`T "- Updating XML db ...");
+(* logger `BR; *)
List.iter
(function
| l when is_blank_line l -> () (* skip blank and commented lines *)
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
| [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 (Lazy.force 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 =
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"
(* 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
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"))
+ ClientHTTP.get_and_save_to_tmp
+ (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"))
(* API *)
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 update () =
+let unregister uri =
if remote () then
- update_remote ()
+ unregister_remote uri
else
- update_from_all_servers ()
+ try
+ (map_of_uri uri)#remove uri
+ with Key_not_found _ -> ()
-let getxml ?(format = Enc_normal) ?(patch_dtd = true) uri =
+let update ?(logger = fun _ -> ()) () =
+ if remote () then
+ update_remote logger ()
+ else
+ update_from_all_servers logger ()
+
+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 ~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
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
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
if remote () then
list_servers_remote ()
else
- Lazy.force Http_getter_env.servers
+ 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
- List.assoc position (Lazy.force Http_getter_env.servers)
+ List.assoc position (Http_getter_env.servers ())
with Not_found ->
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 =
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
"^([^.]*\\.[^.]*)((\\.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
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
ls_items :=
Ls_object {
uri = uri; ann = annflag;
- types = typesflag; body = typesflag; proof_tree = treeflag
+ types = typesflag; body = bodyflag; proof_tree = treeflag
} :: !ls_items)
objs;
List.rev !ls_items
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 ()
projects / helm.git / blobdiff