]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/registry/helm_registry.ml
Bug fixed in computation of the domain of records with left parameters.
[helm.git] / helm / ocaml / registry / helm_registry.ml
index 7767e4da269dc8e749aeebaf6937b1bf1cf0f602..42316a27f8dd26c977bf55b7c4e8638920177f1f 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 let debug = false
 let debug_print s =
-  if debug then prerr_endline ("Helm_registry debugging: " ^ s)
+  if debug then prerr_endline ("Helm_registry debugging: " ^ (Lazy.force s))
 
   (** <helpers> *)
 
@@ -117,10 +119,11 @@ let key_is_valid key =
   if not (Str.string_match valid_key_rex key 0) then
     raise (Malformed_key key)
 
-let set' registry ~key ~value =
-  debug_print (sprintf "Setting %s = %s" key value);
+let set' ?(replace=false) registry ~key ~value =
+  debug_print (lazy(sprintf "Setting (replace: %b) %s = %s" replace key value));
   key_is_valid key;
-  Hashtbl.add registry key value
+  let add_fun = if replace then Hashtbl.replace else Hashtbl.add in
+  add_fun registry key value
 
 let unset registry = Hashtbl.remove registry
 
@@ -163,8 +166,6 @@ let get registry key =
   in
   List.map strip_blanks (aux [] key)
 
-let set registry = set' registry
-
 let has registry key = Hashtbl.mem registry key
 
 let get_typed registry unmarshaller key =
@@ -172,7 +173,7 @@ let get_typed registry unmarshaller key =
   unmarshaller value
 
 let set_typed registry marshaller ~key ~value =
-  set registry ~key ~value:(marshaller value)
+  set' ~replace:true registry ~key ~value:(marshaller value)
 
 let get_opt registry unmarshaller key =
   try
@@ -187,7 +188,7 @@ let get_opt_default registry unmarshaller ~default key =
 let set_opt registry marshaller ~key ~value =
   match value with
   | None -> unset registry key
-  | Some value -> set registry ~key ~value:(marshaller value)
+  | Some value -> set' ~replace:true registry ~key ~value:(marshaller value)
 
 let get_list registry unmarshaller key =
   try
@@ -201,7 +202,10 @@ let get_pair registry fst_unmarshaller snd_unmarshaller key =
   | _ -> raise (Type_error "not a pair")
 
 let set_list registry marshaller ~key ~value =
-  List.iter (fun v -> set registry ~key ~value:(marshaller v)) value
+  Hashtbl.remove registry key;
+  List.iter
+    (fun v -> set' ~replace:false registry ~key ~value:(marshaller v))
+    value
 
 type xml_tree =
   | Cdata of string
@@ -275,7 +279,7 @@ let rec load_from_absolute ?path registry fname =
     | "key", ["name", name] -> in_key := true; push_path name
     | "helm_registry", _ -> ()
     | "include", ["href", fname] ->
-        debug_print ("including file " ^ fname);
+        debug_print (lazy ("including file " ^ fname));
         load_from_absolute ~path:!_path registry fname
     | tag, _ ->
         raise (Parse_error (fname, ~-1, ~-1,
@@ -286,7 +290,7 @@ let rec load_from_absolute ?path registry fname =
     | "section" -> pop_path ()
     | "key" ->
         let key = String.concat "." (List.rev !_path) in
-        set registry ~key ~value:!cdata;
+        set' registry ~key ~value:!cdata;
         cdata := "";
         in_key := false;
         pop_path ()
@@ -304,7 +308,7 @@ let rec load_from_absolute ?path registry fname =
   } in
   let xml_parser = XmlPushParser.create_parser callbacks in
   let backup = backup_registry registry in
-  if path = None then Hashtbl.clear registry;
+(*   if path = None then Hashtbl.clear registry; *)
   try
     XmlPushParser.parse xml_parser (`File fname)
   with exn ->
@@ -387,7 +391,7 @@ let ls registry prefix =
 let default_registry = Hashtbl.create magic_size
 
 let get key = singleton (get default_registry key)
-let set = set default_registry
+let set = set' ~replace:true default_registry
 let has = has default_registry
 let fold ?prefix ?interpolate f init =
   fold default_registry ?prefix ?interpolate f init
@@ -405,6 +409,7 @@ let set_list marshaller = set_list default_registry marshaller
 let unset = unset default_registry
 let save_to = save_to default_registry
 let load_from = load_from default_registry
+let clear () = Hashtbl.clear default_registry
 
 let get_string = get_typed string
 let get_int = get_typed int