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

diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml
index 877de0a1c..08b1bb76f 100644
--- a/matita/components/registry/helm_registry.ml
+++ b/matita/components/registry/helm_registry.ml
@@ -121,6 +121,12 @@ let triple fst_unmarshaller snd_unmarshaller trd_unmarshaller v =
   | [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
@@ -220,6 +226,10 @@ let get_pair registry fst_unmarshaller snd_unmarshaller =
 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
@@ -424,6 +434,7 @@ 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