X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=e03817a22b9f7f68a6cfcf1becc2a1df9884cf43;hb=4e683370099ea7aaea877bc345ca8821938d49ed;hp=982544bce69e606545660e839f7d539b471fb7ac;hpb=1e34c17c30ee6c992f3759bd0f0d5012e6803092;p=helm.git diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index 982544bce..e03817a22 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -88,7 +88,12 @@ let map_of_uri = function | uri when is_xsl_uri uri -> xsl_map | uri -> raise (Http_getter_unresolvable_URI uri) in -let resolve uri = (map_of_uri uri)#resolve uri in +let resolve uri = + try + (map_of_uri uri)#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 return_all_foo_uris map doctype filter outchan = (** return all URIs contained in 'map' which satisfy predicate 'filter'; URIs @@ -342,13 +347,14 @@ let callback (req: Http_types.request) outchan = return_html_msg "Register done" outchan | _ -> assert false) | "/update" -> - (xml_map#clear; rdf_map#clear; xsl_map#clear; + (Http_getter_env.reload (); (* reload servers list from servers file *) + xml_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) + (List.rev !Http_getter_env.servers) in xml_map#sync; rdf_map#sync; xsl_map#sync; return_html_msg log outchan)