From: Stefano Zacchiroli Date: Mon, 7 Apr 2003 13:34:07 +0000 (+0000) Subject: - added "/add_server" and "/remove_server" to dynamically adjust servers X-Git-Tag: before_refactoring~39 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a4520a0d408ece8a4e3cc1dab3f89e91f01f623d - added "/add_server" and "/remove_server" to dynamically adjust servers list at runtime --- diff --git a/helm/http_getter/ChangeLog b/helm/http_getter/ChangeLog index 6de4c521b..58efbc09e 100644 --- a/helm/http_getter/ChangeLog +++ b/helm/http_getter/ChangeLog @@ -1,2 +1,5 @@ -08/01/2003: OCaml reimplementation available! +- added "add_server", "remove_server" methods +- bugfix: multiple definition of URI by different servers are now permitted + +08/01/2003: OCaml reimplementation available! (version 0.2.1) 28/12/2000: First alpha release diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index 26b0774a4..d8526afa9 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -105,7 +105,10 @@ let resolve uri = with Http_getter_map.Key_not_found _ -> raise (Http_getter_unresolvable_URI uri) in -let register uri = (map_of_uri uri )#add uri in +let register uri = + (* Warning: this fail if uri is already registered *) + (map_of_uri uri)#add uri +in let return_all_foo_uris map doctype filter outchan = (** return all URIs contained in 'map' which satisfy predicate 'filter'; URIs are written in an XMLish format ('doctype' is the XML doctype) onto 'outchan' @@ -290,10 +293,12 @@ let update_from_server logmsg server_url = (* use global maps *) (match Pcre.split ~rex:index_line_sep_RE l with | [uri; "gz"] -> assert (is_cic_uri uri || is_nuprl_uri uri) ; - (map_of_uri uri)#add uri ((xml_url_of_uri uri) ^ ".xml.gz") + (map_of_uri uri)#replace + uri ((xml_url_of_uri uri) ^ ".xml.gz") | [uri] -> assert (is_cic_uri uri || is_nuprl_uri uri) ; - (map_of_uri uri)#add uri ((xml_url_of_uri uri) ^ ".xml") + (map_of_uri uri)#replace + uri ((xml_url_of_uri uri) ^ ".xml") | _ -> log := !log ^ "Ignoring invalid line: '" ^ l ^ "'
\n") with Http_getter_invalid_URI uri -> @@ -307,8 +312,9 @@ let update_from_server logmsg server_url = (* use global maps *) (fun l -> try (match Pcre.split ~rex:index_line_sep_RE l with - | [uri; "gz"] -> rdf_map#add uri ((rdf_url_of_uri uri) ^ ".xml.gz") - | [uri] -> rdf_map#add uri ((rdf_url_of_uri uri) ^ ".xml") + | [uri; "gz"] -> + rdf_map#replace uri ((rdf_url_of_uri uri) ^ ".xml.gz") + | [uri] -> rdf_map#replace uri ((rdf_url_of_uri uri) ^ ".xml") | _ -> log := !log ^ "Ignoring invalid line: " ^ l ^ "
\n") with Http_getter_invalid_URI uri -> log := !log ^ "Ignoring invalid RDF URI: " ^ uri ^ "
\n") @@ -318,13 +324,25 @@ let update_from_server logmsg server_url = (* use global maps *) | Some xsl_index -> (log := !log ^ "Updating XSLT db ...
\n"; List.iter - (fun l -> xsl_map#add l (server_url ^ "/" ^ l)) + (fun l -> xsl_map#replace l (server_url ^ "/" ^ l)) (Pcre.split ~rex:index_sep_RE xsl_index); log := !log ^ "All done!
\n") | None -> ()); debug_print "done with this server"; !log in +let update_from_all_servers () = (* use global maps *) + cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear; + let log = + List.fold_left + update_from_server + "" (* initial logmsg: empty *) + (* 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; + log +in (* thread action *) @@ -365,17 +383,65 @@ let callback (req: Http_types.request) outchan = return_html_msg "Register done" outchan | _ -> assert false) | "/update" -> - (Http_getter_env.reload (); (* reload servers list from servers file *) - cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear; - let log = - List.fold_left - update_from_server - "" (* initial logmsg: empty *) - (* reverse order: 1st server is the most important one *) - (List.rev !Http_getter_env.servers) + Http_getter_env.reload (); (* reload servers list from servers file *) + let log = update_from_all_servers () in + return_html_msg log outchan + | "/add_server" -> + let name = req#param "url" in + (try + let position = + try + let res = int_of_string (req#param "position") in + if res < 0 then + raise (Failure "int_of_string"); + res + with Failure "int_of_string" -> + raise (Http_getter_bad_request + (sprintf "position must be a non negative integer (%s given)" + (req#param "position"))) + in + if position = 0 then (* fallback to default value *) + raise (Http_types.Param_not_found "foo") + else if position > 0 then begin (* add server and update all *) + Http_getter_env.add_server ~position name; + let log = update_from_all_servers () in + return_html_msg + (sprintf "Added server %s in position %d)
\n%s" + name position log) + outchan + end else (* position < 0 *) (* error! *) + assert false (* already checked above *) + with Http_types.Param_not_found _ -> (* add as 1st server by default *) + Http_getter_env.add_server ~position:0 name; + let log = update_from_server (* quick update (new server only) *) + (sprintf "Added server %s in head position
\n" name) name + in + return_html_msg log outchan) + | "/remove_server" -> + let position = + try + let res = int_of_string (req#param "position") in + if res < 0 then + raise (Failure "int_of_string"); + res + with Failure "int_of_string" -> + raise (Http_getter_bad_request + (sprintf "position must be a non negative integer (%s given)" + (req#param "position"))) + in + let server_name = + try + List.nth !Http_getter_env.servers position + with Failure "nth" -> + raise (Http_getter_bad_request + (sprintf "no server with position %d" position)) in - cic_map#sync; nuprl_map#sync; rdf_map#sync; xsl_map#sync; - return_html_msg log outchan) + Http_getter_env.remove_server position; + let log = update_from_all_servers () in + return_html_msg + (sprintf "Removed server %s (position %d)
\n%s" + server_name position log) + outchan | "/getalluris" -> return_all_xml_uris (fun uri ->