add_leaf -> application methode cache

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@204 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 10 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 075e0e12a..b9964a87f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,8 +26,6 @@ type library_entry = section_path * node
 
 let lib_stk = ref ([] : (section_path * node) list)
 
-let lib_tab = Hashtbl.create 353
-
 let module_name = ref None
 let path_prefix = ref ([] : string list)
 
@@ -71,8 +69,7 @@ let split_lib sp =
 (* Adding operations. *)
 
 let add_entry sp node =
-  lib_stk := (sp,node) :: !lib_stk;
-  Hashtbl.add lib_tab sp node
+  lib_stk := (sp,node) :: !lib_stk
 
 let anonymous_id = 
   let n = ref 0 in
@@ -86,10 +83,12 @@ let add_anonymous_entry node =
 let add_leaf id kind obj =
   let sp = make_path id kind in
   add_entry sp (Leaf obj);
+  cache_object (sp,obj);
   sp
 
 let add_anonymous_leaf obj =
-  add_anonymous_entry (Leaf obj)
+  let sp = add_anonymous_entry (Leaf obj) in
+  cache_object (sp,obj)
 
 let add_frozen_state () =
   let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
@@ -98,11 +97,6 @@ let contents_after = function
   | None -> !lib_stk
   | Some sp -> let (after,_,_) = split_lib sp in after
 
-let map_leaf sp = 
-  match Hashtbl.find lib_tab sp with
-    | Leaf obj -> obj
-    | _ -> anomaly "Lib.map_leaf: not a leaf"
-
 (* Sections. *)
 
 let open_section s =
@@ -178,6 +172,10 @@ let reset_to sp =
   let (after,_,_) = split_lib spf in
   recache_context (List.rev after)
 
+let reset_name id =
+  let (sp,_) = find_entry_p (fun (sp,_) -> id = basename sp) in
+  reset_to sp
+
 let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
 
 (* State and initialization. *)