From e7ab167b72dc48d260d82060949e8ebe7d27764c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 Dec 2002 19:30:00 +0000 Subject: [PATCH] - added maps sync --- helm/http_getter/http_getter.ml | 5 ++--- helm/http_getter/http_getter_map.ml | 6 ++++++ helm/http_getter/http_getter_map.mli | 1 + 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index c46a79326..c5d4f169d 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -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 diff --git a/helm/http_getter/http_getter_map.ml b/helm/http_getter/http_getter_map.ml index 07c2c10b4..7a5ed1a3b 100644 --- a/helm/http_getter/http_getter_map.ml +++ b/helm/http_getter/http_getter_map.ml @@ -66,6 +66,12 @@ class map dbname = Dbm.iter f db )) + method sync = + self#doWriter (lazy ( + Dbm.close db; + db <- open_dbm () + )) + method clear = self#doWriter (lazy ( Dbm.close db; diff --git a/helm/http_getter/http_getter_map.mli b/helm/http_getter/http_getter_map.mli index d3402eea3..3e0cd0878 100644 --- a/helm/http_getter/http_getter_map.mli +++ b/helm/http_getter/http_getter_map.mli @@ -34,5 +34,6 @@ class map: method remove: string -> unit method resolve: string -> string method iter: (string -> string -> unit) -> unit + method sync: unit method clear: unit end -- 2.39.2