From: Enrico Tassi 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 =