diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/library/lib.ml b/library/lib.ml index 075e0e12af..b9964a87f9 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. *) |