From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 28 Jun 2005 08:19:36 +0000 (+0000)
Subject: added get_pair method
X-Git-Tag: INDEXING_NO_PROOFS~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e510bddb3826ec421b1e5f22ce972430994a410c;p=helm.git

added get_pair method
---

diff --git a/helm/ocaml/registry/helm_registry.ml b/helm/ocaml/registry/helm_registry.ml
index 501f689d8..0b54116cb 100644
--- a/helm/ocaml/registry/helm_registry.ml
+++ b/helm/ocaml/registry/helm_registry.ml
@@ -62,7 +62,6 @@ exception Key_not_found of string
 exception Cyclic_definition of string
 exception Type_error of string (* expected type, value, msg *)
 exception Parse_error of string * int * int * string  (* file, line, col, msg *)
-exception Invalid_value of (string * string) * string (* key, value, descr *)
 
   (* root XML tag: used by save_to, ignored by load_from *)
 let root_tag = "helm_registry"
@@ -195,6 +194,12 @@ let get_list registry unmarshaller key =
     List.map unmarshaller (get registry key)
   with Key_not_found _ -> []
 
+let get_pair registry unmarshaller key =
+  let v = singleton (get registry key) in
+  match Str.split spaces_rex v with
+  | [fst; snd] -> unmarshaller fst, unmarshaller snd
+  | _ -> raise (Type_error "not a pair")
+
 let set_list registry marshaller ~key ~value =
   List.iter (fun v -> set registry ~key ~value:(marshaller v)) value
 
@@ -389,6 +394,7 @@ let get_typed unmarshaller = get_typed default_registry unmarshaller
 let get_opt unmarshaller = get_opt default_registry unmarshaller
 let get_opt_default unmarshaller = get_opt_default default_registry unmarshaller
 let get_list unmarshaller = get_list default_registry unmarshaller
+let get_pair unmarshaller = get_pair default_registry unmarshaller
 let set_typed marshaller = set_typed default_registry marshaller
 let set_opt unmarshaller = set_opt default_registry unmarshaller
 let set_list marshaller = set_list default_registry marshaller
diff --git a/helm/ocaml/registry/helm_registry.mli b/helm/ocaml/registry/helm_registry.mli
index e9ee901e8..7dd2a68d4 100644
--- a/helm/ocaml/registry/helm_registry.mli
+++ b/helm/ocaml/registry/helm_registry.mli
@@ -88,11 +88,6 @@ exception Malformed_key of string
    *)
 exception Parse_error of string * int * int * string
 
-  (** raised when a given <key,value> pair fails validity test(s)
-   * @param pair <key,value> pair
-   * @param descr description of the failed test *)
-exception Invalid_value of (string * string) * string
-
 (** {2 Generic untyped interface}
  * Using the functions below this module could be used as a repository of
  * key/value pairs *)
@@ -151,6 +146,9 @@ val get_opt_default: (string -> 'a) -> default:'a -> string -> 'a
   (** never fails with Key_not_found, instead return the empty list *)
 val get_list: (string -> 'a) -> string -> 'a list
 
+  (** same as get_list, but assumes list length to be 2 *)
+val get_pair: (string -> 'a) -> string -> 'a * 'a
+
 (** {4 Shorthands} *)
 
 val get_string: string -> string
diff --git a/helm/ocaml/registry/tests/sample.xml b/helm/ocaml/registry/tests/sample.xml
index e8ebdc76b..d08ce5644 100644
--- a/helm/ocaml/registry/tests/sample.xml
+++ b/helm/ocaml/registry/tests/sample.xml
@@ -17,6 +17,7 @@
     <key name="int_list">13</key>
     <key name="int_list">17</key>
     <key name="int_list">19</key>
+    <key name="int_pair">19 23</key>
   </section>
   <section name="triciclo">
     <section name="foo1">