]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/registry/helm_registry.ml
helm_registry: added the pair unmarshaller
[helm.git] / helm / software / components / registry / helm_registry.ml
index b7b3de11d6c48eb4c269da61cd0b60cb07e3d36a..3753232b6a01d1da8f00f2f9a1044d7aebda1d95 100644 (file)
@@ -109,6 +109,12 @@ let of_int = handle_type_error string_of_int
 let of_float = handle_type_error string_of_float
 let of_bool = handle_type_error string_of_bool
 
+(* FG *)
+let pair fst_unmarshaller snd_unmarshaller v =
+  match Str.split spaces_rex v with
+  | [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd
+  | _ -> raise (Type_error "not a pair")
+
   (* escapes for xml configuration file *)
 let (escape, unescape) =
   let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in
@@ -198,11 +204,9 @@ let get_list registry unmarshaller key =
     List.map unmarshaller (get registry key)
   with Key_not_found _ -> []
 
-let get_pair registry fst_unmarshaller snd_unmarshaller key =
-  let v = singleton (get registry key) in
-  match Str.split spaces_rex v with
-  | [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd
-  | _ -> raise (Type_error "not a pair")
+(* FG *)
+let get_pair registry fst_unmarshaller snd_unmarshaller =
+  get_typed registry (pair fst_unmarshaller snd_unmarshaller) 
 
 let set_list registry marshaller ~key ~value =
   Hashtbl.remove registry key;