]> matita.cs.unibo.it Git - helm.git/commitdiff
- use polymorphic variants for some configuration parameters
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 09:52:10 +0000 (09:52 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 09:52:10 +0000 (09:52 +0000)
helm/ocaml/getter/http_getter_env.ml
helm/ocaml/getter/http_getter_types.ml

index 3264d6c65c33c546f6acae91acf0a20239627b39..985faee9bd346bde407e179d28fe035971725a32 100644 (file)
@@ -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 ())))
index 74ffe9fe1ee45eaae21f8e94fdc9998d693ef7aa..172cf18a963e3f2cea18aa586e9347b022f5b6d3 100644 (file)
@@ -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 =
   {