From: Stefano Zacchiroli Date: Mon, 7 Apr 2003 13:33:42 +0000 (+0000) Subject: - added functions "add_server" and "remove_server" to dynamically adjust X-Git-Tag: before_refactoring~40 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4a44fbdb0e13c8d515f62d33e33e6b8cc519d74f;p=helm.git - added functions "add_server" and "remove_server" to dynamically adjust servers list at runtime --- diff --git a/helm/http_getter/http_getter_env.ml b/helm/http_getter/http_getter_env.ml index 661b4ae47..a531cfa75 100644 --- a/helm/http_getter/http_getter_env.ml +++ b/helm/http_getter/http_getter_env.ml @@ -151,5 +151,20 @@ servers: cic_dir nuprl_dir rdf_dir dtd_dir servers_file host port my_own_url dtd_base_url (match cache_mode with Enc_normal -> "Normal" | Enc_gzipped -> "GZipped") - conf_file conf_dir (String.concat "\n\t" !servers) + conf_file conf_dir + (String.concat "\n\t" (* servers list prepended with server number *) + (List.map + (let idx = ref ~-1 in + fun server -> incr idx; sprintf "%3d: %s" !idx server) + !servers)) + +let add_server ?position url = + (match position with + | Some p -> Http_getter_misc.add_line ~fname:servers_file ~position:p url + | None -> Http_getter_misc.add_line ~fname:servers_file url); + reload_servers () + +let remove_server position = + Http_getter_misc.remove_line ~fname:servers_file position; + reload_servers () diff --git a/helm/http_getter/http_getter_env.mli b/helm/http_getter/http_getter_env.mli index 41028389d..6d4d6312f 100644 --- a/helm/http_getter/http_getter_env.mli +++ b/helm/http_getter/http_getter_env.mli @@ -28,11 +28,11 @@ open Http_getter_types;; - (* general information *) + (* {2 general information} *) val version : string (* getter version *) - (* environment gathered data *) + (* {2 environment gathered data} *) val cic_dbm : string (* XML map DBM file for CIC *) val nuprl_dbm : string (* XML map DBM file for NuPRL *) @@ -49,19 +49,29 @@ val servers_file : string (* servers.txt file *) val port : int (* port on which getter listens *) val dtd_base_url : string (* base URL for DTD downloading *) - (* derived data *) + (* {2 derived data} *) val host : string (* host on which getter listens *) val my_own_url : string (* URL at which contact getter *) -val servers : string list ref (* servers list *) +val servers : string list ref (* servers list. DO NOT CHANGE this list, + modifications wont be preserved *) val cache_mode : http_getter_encoding (* cached files encoding *) val conf_file : string (* configuration file's full path *) val conf_dir : string (* directory where conf_file resides *) - (* misc *) + (* {2 dynamic configuration changes} *) -val reload: unit -> unit (* reload servers list *) + (* add a server to servers list in a given position (defaults to "after the + last server", change servers file accordingly and reload servers list *) +val add_server: ?position:int -> string -> unit + (* remove a server from servers list, change servers file accordingly and + reload servers list *) +val remove_server: int -> unit + + (* {2 misc} *) + +val reload: unit -> unit (* reload configuration information *) val env_to_string : unit -> string (* dump a textual representation of the current http_getter settings on an output - channel*) + channel *)