From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 16 Apr 2004 08:17:38 +0000 (+0000)
Subject: - added sample usage of get_opt method
X-Git-Tag: dead_dir_walking~58
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e9f24f9763283b44fcef456177f0390b51db7779

- added sample usage of get_opt method
- added method get_opt_default (like get_opt with an additional default
  value)
---

diff --git a/helm/ocaml/registry/helm_registry.ml b/helm/ocaml/registry/helm_registry.ml
index 5569165a3..35273608f 100644
--- a/helm/ocaml/registry/helm_registry.ml
+++ b/helm/ocaml/registry/helm_registry.ml
@@ -167,6 +167,10 @@ let set_opt setter ~key ~value =
   match value with
   | None -> unset key
   | Some value -> setter ~key ~value
+let get_opt_default getter default key =
+  match get_opt getter key with
+  | None -> default
+  | Some v -> v
 
 let add_validator ~key ~validator ~descr =
   let id = get_next_validator_id () in
diff --git a/helm/ocaml/registry/helm_registry.mli b/helm/ocaml/registry/helm_registry.mli
index e1c0289a5..1f40b5453 100644
--- a/helm/ocaml/registry/helm_registry.mli
+++ b/helm/ocaml/registry/helm_registry.mli
@@ -133,6 +133,12 @@ val set_string_list:  key:string -> value:string list -> unit
  * set_* function above. Returned value is a get (set) function typed as the
  * given getter (setter) whith optional values. None is returned for missing
  * keys and None can be assigned to a key removing it from the registry.
+ *
+ * Sample  usage:
+ *
+ *  match Helm_registry.get_opt Helm_registry.get_int "foo.bar" with
+ *  | Some i -> ...
+ *  | None -> ...
  *)
 
 val get_opt:
@@ -141,6 +147,8 @@ val get_opt:
 val set_opt:
   (key:string -> value:'a -> unit) (* setter *) ->
     key:string -> value:'a option -> unit
+val get_opt_default:  (* as get_opt with an additional default value *)
+  (string -> 'a) -> 'a -> string -> 'a
 
 (** {2 Validators}
  * Each key may have zero or more associated validators, that are predicates