X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.ml;h=ec6564249270e627d40facb4a9af47c9670bfa95;hb=8004125685a99b6c0f2f95fd7f3fa09a4f5c9094;hp=ac8b98305b2c392450da5fe3629a9c6d30284f2e;hpb=b2c29f8bef99b45f71bc0c5ee656304094d16113;p=helm.git

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index ac8b98305..ec6564249 100644
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -95,8 +95,11 @@ let nuprl_map = new Http_getter_map.map Http_getter_env.nuprl_dbm in
 let rdf_map = new Http_getter_map.map Http_getter_env.rdf_dbm in
 let xsl_map = new Http_getter_map.map Http_getter_env.xsl_dbm in
 
-let save_maps () =
- cic_map#close; nuprl_map#close; rdf_map#close; xsl_map#close in
+let maps = [ cic_map; nuprl_map; rdf_map; xsl_map ] in
+let close_maps () = List.iter (fun m -> m#close) maps in
+let clear_maps () = List.iter (fun m -> m#clear) maps in
+let sync_maps () = List.iter (fun m -> m#sync) maps in
+
 let map_of_uri = function
   | uri when is_cic_uri uri -> cic_map
   | uri when is_nuprl_uri uri -> nuprl_map
@@ -152,13 +155,13 @@ let return_ls =
   in
   let basepart_RE =
     Pcre.regexp
-      "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?"
+      "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
   in
   let (types_RE, types_ann_RE, body_RE, body_ann_RE,
        proof_tree_RE, proof_tree_ann_RE) =
-    (Pcre.regexp "\\.types", Pcre.regexp "\\.types\\.ann",
-     Pcre.regexp "\\.body", Pcre.regexp "\\.body.ann",
-     Pcre.regexp "\\.proof_tree", Pcre.regexp "\\.proof_tree\\.ann")
+    (Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
+     Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
+     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$")
   in
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
@@ -350,7 +353,7 @@ let update_from_server logmsg server_url = (* use global maps *)
   !log
 in
 let update_from_all_servers () =  (* use global maps *)
-  cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear;
+  clear_maps ();
   let log =
     List.fold_left
       update_from_server
@@ -358,7 +361,7 @@ let update_from_all_servers () =  (* use global maps *)
         (* 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;
+  sync_maps ();
   log
 in
 
@@ -523,12 +526,12 @@ let main () =
   print_string (Http_getter_env.env_to_string ());
   flush stdout;
   Unix.putenv "http_proxy" "";
-  at_exit save_maps;
+  at_exit close_maps;
   Sys.catch_break true;
   try
     Http_daemon.start'
       ~timeout:(Some 600) ~port:Http_getter_env.port ~mode:`Thread callback
-  with Sys.Break -> ()  (* 'save_maps' already registered with 'at_exit' *)
+  with Sys.Break -> ()  (* 'close_maps' already registered with 'at_exit' *)
 in
 
 main ()