]> matita.cs.unibo.it Git - helm.git/commitdiff
A lazy value was put in place of a function ==> the memoized value was no
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Feb 2004 18:36:54 +0000 (18:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Feb 2004 18:36:54 +0000 (18:36 +0000)
longer updated. Fixed.

helm/ocaml/getter/http_getter.ml
helm/ocaml/getter/http_getter_env.ml
helm/ocaml/getter/http_getter_env.mli

index 38683430d106c99d5da66d2d3fd2e23327c99cf0..21ed483ad157bc64de0abe11bdf4b100766d3908 100644 (file)
@@ -164,7 +164,7 @@ let update_from_all_servers () =  (* use global maps *)
       update_from_server
       []  (* initial logmsg: empty *)
         (* reverse order: 1st server is the most important one *)
-      (List.map snd (List.rev (Lazy.force Http_getter_env.servers)))
+      (List.map snd (List.rev (Http_getter_env.servers ())))
   in
   sync_maps ();
   `Msg (`L (List.rev log))
@@ -309,7 +309,7 @@ let list_servers () =
   if remote () then
     list_servers_remote ()
   else
-    Lazy.force Http_getter_env.servers
+    Http_getter_env.servers ()
 
 let add_server ?(position = 0) name =
   if remote () then
@@ -331,7 +331,7 @@ let remove_server position =
   else begin
     let server_name =
       try
-        List.assoc position (Lazy.force Http_getter_env.servers)
+        List.assoc position (Http_getter_env.servers ())
       with Not_found ->
         raise (Invalid_argument (sprintf "no server with position %d" position))
     in
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 ()
 
index cb1731792e1140fa5fa733367bc67b37802576d5..f55867c923cb406be218b78364980a2197ded56c 100644 (file)
@@ -53,7 +53,7 @@ val dtd_base_url  : string lazy_t         (* base URL for DTD downloading *)
 
 val host          : string lazy_t         (* host on which getter listens *)
 val my_own_url    : string lazy_t         (* URL at which contact getter *)
-val servers       : (int * string) list lazy_t
+val servers       : unit -> (int * string) list
                                     (* (position * server) list *)
 val cache_mode    : encoding lazy_t       (* cached files encoding *)