From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 26 Dec 2002 19:30:00 +0000 (+0000)
Subject: - added maps sync
X-Git-Tag: v0_3_99~114
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e7ab167b72dc48d260d82060949e8ebe7d27764c

- added maps sync
---

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