From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 23 Nov 2007 15:26:03 +0000 (+0000)
Subject: fast and sound registry lists
X-Git-Tag: 0.4.98@7921~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c02c88bdbeb81b379cc7d3e9c875a106a745f5ef;p=helm.git

fast and sound registry lists
faster matitamake setup
---

diff --git a/components/registry/helm_registry.ml b/components/registry/helm_registry.ml
index 64277415f..fd0df5013 100644
--- a/components/registry/helm_registry.ml
+++ b/components/registry/helm_registry.ml
@@ -201,7 +201,9 @@ let set_opt registry marshaller ~key ~value =
 
 let get_list registry unmarshaller key =
   try
-    List.map unmarshaller (get registry key)
+    let tmp = get registry key in
+    let rc = List.map unmarshaller tmp in
+    rc
   with Key_not_found _ -> []
 
 (* FG *)
@@ -209,10 +211,11 @@ 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;
-  List.iter
-    (fun v -> set' ~replace:false registry ~key ~value:(marshaller v))
-    value
+  (* since ocaml hash table are crazy... *)
+  while Hashtbl.mem registry key do
+    Hashtbl.remove registry key
+  done;
+  List.iter (fun v -> set' registry ~key ~value:(marshaller v)) value
 
 type xml_tree =
   | Cdata of string
diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index 2bf01f897..499d0eaf3 100644
--- a/matita/matitamakeLib.ml
+++ b/matita/matitamakeLib.ml
@@ -78,25 +78,26 @@ let initialize () =
   match ls_dir (pool ()) with
   | None -> logger `Error ("Unable to list directory " ^ pool ()) 
   | Some l -> 
-      List.iter 
-        (fun name -> 
-          let root = 
-            try 
-              Some (HExtlib.input_file (pool () ^ name ^ rootfile))
-            with Unix.Unix_error _ -> 
-              logger `Warning ("Malformed development " ^ name);
-              None
-          in 
-          match root with 
-          | None -> ()
-          | Some root -> 
-              developments := {root = root ; name = name} :: !developments;
-              let inc = Helm_registry.get_list 
-                Helm_registry.string "matita.includes" in
-              Helm_registry.set_list Helm_registry.of_string 
-                ~key:"matita.includes" ~value:(inc @ [root])
-          ) 
-      l
+      let paths = 
+        List.fold_left 
+          (fun acc name -> 
+            let root = 
+              try 
+                Some (HExtlib.input_file (pool () ^ name ^ rootfile))
+              with Unix.Unix_error _ -> 
+                logger `Warning ("Malformed development " ^ name);
+                None
+            in 
+            match root with 
+            | None -> acc
+            | Some root -> 
+                developments := {root = root ; name = name} :: !developments;
+                root::acc)
+         [] l
+      in
+      let inc = Helm_registry.get_list Helm_registry.string "matita.includes" in
+      Helm_registry.set_list Helm_registry.of_string 
+        ~key:"matita.includes" ~value:(inc @ paths)
 
 (* finds the makefile path for development devel *)
 let makefile_for_development devel =