From d8738e52af861cbdda5268671b30183b99d51c54 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 6 Apr 2004 09:52:10 +0000 Subject: [PATCH] - use polymorphic variants for some configuration parameters --- helm/ocaml/getter/http_getter_env.ml | 8 +++++--- helm/ocaml/getter/http_getter_types.ml | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml index 3264d6c65..985faee9b 100644 --- a/helm/ocaml/getter/http_getter_env.ml +++ b/helm/ocaml/getter/http_getter_env.ml @@ -92,8 +92,8 @@ let my_own_url = let cache_mode = lazy (match String.lowercase (Helm_registry.get "getter.cache_mode") with - | "normal" -> Enc_normal - | "gz" -> Enc_gzipped + | "normal" -> `Normal + | "gz" -> `Gzipped | mode -> failwith ("Invalid cache mode: " ^ mode)) let reload () = reload_servers () @@ -129,7 +129,9 @@ servers: (Lazy.force dtd_dir) (Lazy.force servers_file) (Lazy.force host) (Lazy.force port) (Lazy.force my_own_url) (Lazy.force dtd_base_url) - (match Lazy.force cache_mode with Enc_normal -> "Normal" | Enc_gzipped -> "GZipped") + (match Lazy.force cache_mode with + | `Normal -> "Normal" + | `Gzipped -> "GZipped") (String.concat "\n\t" (* (position * server) list *) (List.map (fun (pos, server) -> sprintf "%3d: %s" pos server) (servers ()))) diff --git a/helm/ocaml/getter/http_getter_types.ml b/helm/ocaml/getter/http_getter_types.ml index 74ffe9fe1..172cf18a9 100644 --- a/helm/ocaml/getter/http_getter_types.ml +++ b/helm/ocaml/getter/http_getter_types.ml @@ -35,8 +35,8 @@ exception Internal_error of string exception Cache_failure of string exception Dtd_not_found of string (* dtd's url *) -type encoding = Enc_normal | Enc_gzipped -type answer_format = Fmt_text | Fmt_xml +type encoding = [ `Normal | `Gzipped ] +type answer_format = [ `Text | `Xml ] type ls_flag = No | Yes | Ann type ls_object = { -- 2.39.2