X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=0644fcc7d11000003aa8808c770cdebc1bf083ee;hb=b6856f3de223e50ebeb3c26fd098ab128a5d661f;hp=c46a793268911ea98ab702dc7dfb48ef159f3691;hpb=0dc01969c5bdf943e0b84e134b320d1fd39f5e8f;p=helm.git diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index c46a79326..0644fcc7d 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -239,7 +239,7 @@ let update_from_server logmsg server_url = (* use global maps *) Pcre.replace ~pat:"^helm:rdf.*//theory:" ~templ:server_url uri | uri -> raise (Http_getter_invalid_URI uri) in - let log = ref ("Processing server: " ^ server_url ^ "
\n") in + let log = ref (logmsg ^ "Processing server: " ^ server_url ^ "
\n") in let (xml_index, rdf_index, xsl_index) = (* TODO keeps index in memory, is better to keep them on temp files? *) (http_get (server_url ^ "/" ^ Http_getter_env.xml_index), @@ -328,9 +328,7 @@ 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; + (xml_map#clear; rdf_map#clear; xsl_map#clear; let log = List.fold_left update_from_server @@ -338,6 +336,7 @@ let callback (req: Http_types.request) outchan = (* reverse order: 1st server is the most important one *) (List.rev Http_getter_env.servers) in + xml_map#sync; rdf_map#sync; xsl_map#sync; return_html_msg log outchan) | "/getalluris" -> return_all_xml_uris