diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 57 |
1 files changed, 29 insertions, 28 deletions
diff --git a/library/lib.ml b/library/lib.ml index ba6b9c79..09200a5c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 8852 2006-05-23 17:52:43Z notin $ *) +(* $Id: lib.ml 9133 2006-09-12 14:52:07Z notin $ *) open Pp open Util @@ -186,9 +186,9 @@ let add_leaf id obj = if fst (current_prefix ()) = initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in - cache_object (oname,obj); - add_entry oname (Leaf obj); - oname + cache_object (oname,obj); + add_entry oname (Leaf obj); + oname let add_leaves id objs = let oname = make_oname id in @@ -319,7 +319,7 @@ let end_compilation dir = | _, OpenedModtype _ -> error "There are some open module types" | _ -> assert false with - Not_found -> () + Not_found -> () in let module_p = function (_,CompilingLibrary _) -> true | x -> is_something_opened x @@ -331,16 +331,17 @@ let end_compilation dir = with Not_found -> anomaly "No module declared" in - let _ = match !comp_name with + let _ = + match !comp_name with | None -> anomaly "There should be a module name..." | Some m -> if m <> dir then anomaly ("The current open module has name "^ (string_of_dirpath m) ^ - " and not " ^ (string_of_dirpath m)); + " and not " ^ (string_of_dirpath m)); in let (after,_,before) = split_lib oname in - comp_name := None; - !path_prefix,after + comp_name := None; + !path_prefix,after (* Returns true if we are inside an opened module type *) let is_modtype () = @@ -444,15 +445,15 @@ let open_section id = let dir = extend_dirpath olddir id in let prefix = dir, (mp, extend_dirpath oldsec id) in let name = make_path id, make_kn id (* this makes little sense however *) in - if Nametab.exists_section dir then - errorlabstrm "open_section" (pr_id id ++ str " already exists"); - let sum = freeze_summaries() in - add_entry name (OpenedSection (prefix, sum)); - (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); - path_prefix := prefix; - if !Options.xml_export then !xml_open_section id; - add_section () + if Nametab.exists_section dir then + errorlabstrm "open_section" (pr_id id ++ str " already exists"); + let sum = freeze_summaries() in + add_entry name (OpenedSection (prefix, sum)); + (*Pushed for the lifetime of the section: removed by unfrozing the summary*) + Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); + path_prefix := prefix; + if !Options.xml_export then !xml_open_section id; + add_section () (* Restore lib_stk and summaries as before the section opening, and @@ -476,16 +477,16 @@ let close_section id = error "no opened section" in let (secdecls,_,before) = split_lib oname in - lib_stk := before; - let full_olddir = fst !path_prefix in - pop_path_prefix (); - add_entry (make_oname id) ClosedSection; - if !Options.xml_export then !xml_close_section id; - let newdecls = List.map discharge_item secdecls in - Summary.section_unfreeze_summaries fs; - List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls; - Cooking.clear_cooking_sharing (); - Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) + lib_stk := before; + let full_olddir = fst !path_prefix in + pop_path_prefix (); + add_entry (make_oname id) ClosedSection; + if !Options.xml_export then !xml_close_section id; + let newdecls = List.map discharge_item secdecls in + Summary.section_unfreeze_summaries fs; + List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls; + Cooking.clear_cooking_sharing (); + Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) (*****************) (* Backtracking. *) |