X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fregistry%2Fhelm_registry.ml;h=f3309633b72d37748793c21bcfbbb6533f8a59d9;hb=e3369ffc8b690703cfafc7985f69db5fc140d749;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..f3309633b 100644
--- a/matita/components/registry/helm_registry.ml
+++ b/matita/components/registry/helm_registry.ml
@@ -54,7 +54,7 @@ let starts_with prefix =
       String.sub s 0 prefix_len = prefix
     with Invalid_argument _ -> false
 
-let hashtbl_keys tbl = Hashtbl.fold (fun k _ acc -> k :: acc) tbl []
+(*let hashtbl_keys tbl = Hashtbl.fold (fun k _ acc -> k :: acc) tbl []*)
 let hashtbl_pairs tbl = Hashtbl.fold (fun k v acc -> (k,v) :: acc) tbl []
 
   (** </helpers> *)
@@ -85,16 +85,16 @@ let valid_key_rex = Str.regexp ("^" ^ valid_key_rex_raw ^ "$")
 let interpolated_key_rex = Str.regexp ("\\$(" ^ valid_key_rex_raw ^ ")")
 let dot_rex = Str.regexp "\\."
 let spaces_rex = Str.regexp "[ \t\n\r]+"
-let heading_spaces_rex = Str.regexp "^[ \t\n\r]+"
+(*let heading_spaces_rex = Str.regexp "^[ \t\n\r]+"*)
 let margin_blanks_rex =
   Str.regexp "^\\([ \t\n\r]*\\)\\([^ \t\n\r]*\\)\\([ \t\n\r]*\\)$"
 
 let strip_blanks s = Str.global_replace margin_blanks_rex "\\2" s
 
-let split s =
+(*let split s =
   (* trailing blanks are removed per default by split *)
-  Str.split spaces_rex (Str.global_replace heading_spaces_rex "" s)
-let merge l = String.concat " " l
+  Str.split spaces_rex (Str.global_replace heading_spaces_rex "" s)*)
+(*let merge l = String.concat " " l*)
 
 let handle_type_error f x =
   try f x with exn -> raise (Type_error (Printexc.to_string exn))
@@ -121,11 +121,17 @@ 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 (escape, unescape) =
   let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in
   (Netencoding.Html.encode ~in_enc ~out_enc (),
-   Netencoding.Html.decode ~in_enc ~out_enc ~entity_base:`Xml ())
+   Netencoding.Html.decode ~in_enc ~out_enc ~entity_base:`Xml ())*)
 
 let key_is_valid key =
   if not (Str.string_match valid_key_rex key 0) then
@@ -139,7 +145,7 @@ let set' ?(replace=false) registry ~key ~value =
 
 let unset registry = Hashtbl.remove registry
 
-let env_var_of_key s = String.uppercase (Str.global_replace dot_rex "_" s)
+let env_var_of_key s = String.uppercase_ascii (Str.global_replace dot_rex "_" s)
 
 let singleton = function
   | [] ->
@@ -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