From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 library/lib.ml | 57 +++++++++++++++++++++++++++++----------------------------
 1 file changed, 29 insertions(+), 28 deletions(-)

(limited to 'library/lib.ml')

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. *)
-- 
cgit v1.2.3