summaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml57
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. *)