X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fregistry%2Fhelm_registry.ml;h=08b1bb76f893320db7ca6db238bfacb0c16634c2;hb=e83cd27fc0694c34baf35c8b80d32317e51be707;hp=fd0df50136add3246c4e2f1aff7734fad05c0d7f;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml
index fd0df5013..08b1bb76f 100644
--- a/matita/components/registry/helm_registry.ml
+++ b/matita/components/registry/helm_registry.ml
@@ -115,6 +115,18 @@ let pair fst_unmarshaller snd_unmarshaller v =
   | [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd
   | _ -> raise (Type_error "not a pair")
 
+(* FG *)
+let triple fst_unmarshaller snd_unmarshaller trd_unmarshaller v =
+  match Str.split spaces_rex v with
+  | [fst; snd; trd] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd
+  | _ -> raise (Type_error "not a triple")
+
+(* FG *)
+let quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller v =
+  match Str.split spaces_rex v with
+  | [fst; snd; trd; fth] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd, fth_unmarshaller fth
+  | _ -> raise (Type_error "not a quad")
+
   (* escapes for xml configuration file *)
 let (escape, unescape) =
   let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in
@@ -210,6 +222,14 @@ let get_list registry unmarshaller key =
 let get_pair registry fst_unmarshaller snd_unmarshaller =
   get_typed registry (pair fst_unmarshaller snd_unmarshaller) 
 
+(* FG *)
+let get_triple registry fst_unmarshaller snd_unmarshaller trd_unmarshaller =
+  get_typed registry (triple fst_unmarshaller snd_unmarshaller trd_unmarshaller) 
+
+(* FG *)
+let get_quad registry fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller =
+  get_typed registry (quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller) 
+
 let set_list registry marshaller ~key ~value =
   (* since ocaml hash table are crazy... *)
   while Hashtbl.mem registry key do
@@ -413,6 +433,8 @@ 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 get_triple unmarshaller = get_triple default_registry unmarshaller
+let get_quad unmarshaller = get_quad 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