X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_env.mli;h=6d4d6312f2ab726c15bb24523179b652affb2d4e;hb=f15a13bab100064a4da238cede323b8d4568c174;hp=41028389de47d4a3e0320839e2c8028628ee58dc;hpb=bcb3a166855c11d57aee0130df8f666c9db303ec;p=helm.git 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 *)