]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/http_getter_env.ml
A lazy value was put in place of a function ==> the memoized value was no
[helm.git] / helm / ocaml / getter / http_getter_env.ml
index 623be8aef0c9630841ac53ca78679370b33f84a1..3264d6c65c33c546f6acae91acf0a20239627b39 100644 (file)
@@ -53,7 +53,7 @@ let port            = lazy (Helm_registry.get_int "getter.port")
 let _servers = ref None
 
 let servers =
-  lazy
+ function () ->
     (match !_servers with
     | None -> failwith "Getter not yet initialized: servers not available"
     | Some servers -> servers)
@@ -74,7 +74,7 @@ let reload_servers () = _servers := Some (load_servers ())
 let save_servers () =
   let oc = open_out (Lazy.force servers_file) in
   List.iter (fun (_,server) -> output_string oc (server ^ "\n"))
-    (Lazy.force servers);
+    (servers ());
   close_out oc
 
 let host =
@@ -132,11 +132,11 @@ servers:
     (match Lazy.force cache_mode with Enc_normal -> "Normal" | Enc_gzipped -> "GZipped")
     (String.concat "\n\t" (* (position * server) list *)
       (List.map (fun (pos, server) -> sprintf "%3d: %s" pos server)
-        (Lazy.force servers)))
+        (servers ())))
 
 let add_server ?position url =
   let new_servers =
-    let servers = Lazy.force servers in
+    let servers = servers () in
     match position with
     | None -> servers @ [-1, url];
     | Some p when p > 0 ->
@@ -154,7 +154,7 @@ let add_server ?position url =
   reload_servers ()
 
 let remove_server position =
-  _servers := Some (List.remove_assoc position (Lazy.force servers));
+  _servers := Some (List.remove_assoc position (servers ()));
   save_servers ();
   reload_servers ()