certains effets disparaissent a la sortie des sections, d'autres non (selon Summary.survive_section)

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

10 files changed, 42 insertions, 20 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b90dc2215..e1884ed5f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -52,7 +52,8 @@ let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
-	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
+	    Summary.init_function = (fun () -> vartab := Spmap.empty);
+	    Summary.survive_section = false }
 
 let cache_variable (sp,(id,(d,_,_) as vd)) =
   begin match d with (* Fails if not well-typed *)
@@ -114,7 +115,8 @@ let csttab = ref (Spmap.empty : strength Spmap.t)
 let _ = Summary.declare_summary "CONSTANT"
 	  { Summary.freeze_function = (fun () -> !csttab);
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
-	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
+	    Summary.init_function = (fun () -> csttab := Spmap.empty);
+	    Summary.survive_section = false }
 
 let cache_constant (sp,(cdt,stre)) =
   begin match cdt with 
diff --git a/library/global.ml b/library/global.ml
index d5885ed02..2fcd3c2b6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -23,7 +23,8 @@ let _ =
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
-      init_function = (fun () -> global_env := empty_environment) }
+      init_function = (fun () -> global_env := empty_environment);
+      survive_section = true }
 
 (* Then we export the functions of [Typing] on that environment. *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index dc5f994e3..59d0543e2 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -77,7 +77,8 @@ module MakeTable =
 	Summary.declare_summary kn
           { Summary.freeze_function = freeze;
             Summary.unfreeze_function = unfreeze;
-            Summary.init_function = init }
+            Summary.init_function = init;
+	    Summary.survive_section = true }
 
     let (add_option,remove_option) =
       if A.synchronous then
@@ -219,7 +220,8 @@ let _ =
   Summary.declare_summary "Sync_option"
     { Summary.freeze_function = freeze_sync_table;
       Summary.unfreeze_function = unfreeze_sync_table;
-      Summary.init_function = init_sync_table }
+      Summary.init_function = init_sync_table;
+      Summary.survive_section = true }
 
 (* Tools for handling options *)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 6ef403f59..3232c4848 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -314,7 +314,8 @@ let _ =
   Summary.declare_summary "implicits"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let rollback f x =
   let fs = freeze () in
diff --git a/library/lib.ml b/library/lib.ml
index a22f89353..9b5ba27b7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -9,7 +9,7 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of string
-  | OpenedSection of string
+  | OpenedSection of string * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
   | ClosedSection of bool * string * library_segment * Nametab.module_contents
   | FrozenState of Summary.frozen
@@ -103,7 +103,7 @@ let contents_after = function
 
 let open_section s =
   let sp = make_path (id_of_string s) OBJ in
-  add_entry sp (OpenedSection s);
+  add_entry sp (OpenedSection (s, freeze_summaries()));
   path_prefix := !path_prefix @ [s];
   sp
 
@@ -138,10 +138,10 @@ let export_segment seg =
   clean [] seg
 
 let close_section export f s =
-  let sp = 
+  let sp,fs = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection s' -> 
-	  if s <> s' then error "this is not the last opened section"; sp
+      | sp,OpenedSection (s',fs) -> 
+	  if s <> s' then error "this is not the last opened section"; (sp,fs)
       | _ -> assert false
     with Not_found ->
       error "no opened section"
@@ -150,7 +150,7 @@ let close_section export f s =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  let contents = f sp after in
+  let contents = f fs sp after in
   add_entry (make_path (id_of_string s) OBJ)
     (ClosedSection (export, s,after',contents));
   Nametab.push_module s contents;
diff --git a/library/lib.mli b/library/lib.mli
index 96b1941ce..397e5a53b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -14,7 +14,7 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of string
-  | OpenedSection of string
+  | OpenedSection of string * Summary.frozen
   | ClosedSection of bool * string * library_segment * Nametab.module_contents
   | FrozenState of Summary.frozen
 
@@ -41,8 +41,9 @@ val contents_after : section_path option -> library_segment
 
 val open_section : string -> section_path
 val close_section : export:bool ->
-  (section_path -> library_segment -> Nametab.module_contents) -> string
-    -> unit
+  (Summary.frozen -> section_path -> library_segment 
+     -> Nametab.module_contents) 
+  -> string -> unit
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> dir_path
diff --git a/library/library.ml b/library/library.ml
index da7d01895..70cf895e5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -54,7 +54,8 @@ let _ =
   Summary.declare_summary "MODULES"
     { Summary.freeze_function = (fun () -> !modules_table);
       Summary.unfreeze_function = (fun ft -> modules_table := ft);
-      Summary.init_function = (fun () -> modules_table := Stringmap.empty) }
+      Summary.init_function = (fun () -> modules_table := Stringmap.empty);
+      Summary.survive_section = true }
 
 let find_module s =
   try
diff --git a/library/nametab.ml b/library/nametab.ml
index c45e7d93e..de5c22c09 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -77,7 +77,8 @@ let _ =
   Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let rollback f x =
   let fs = freeze () in
diff --git a/library/summary.ml b/library/summary.ml
index 0ba07a737..8fbd5efe4 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -8,7 +8,8 @@ open Names
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit }
+  init_function : unit -> unit;
+  survive_section : bool }
 
 let summaries = 
   (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
@@ -21,7 +22,8 @@ let declare_summary sumname sdecl =
   let ddecl = {
     freeze_function = dyn_freeze;
     unfreeze_function = dyn_unfreeze;
-    init_function = dyn_init} 
+    init_function = dyn_init;
+    survive_section = sdecl.survive_section } 
   in
   if Hashtbl.mem summaries sumname then
     anomalylabstrm "Summary.declare_summary"
@@ -44,5 +46,14 @@ let unfreeze_summaries fs =
        with Not_found -> decl.init_function())
     summaries
 
+let unfreeze_lost_summaries fs =
+  Hashtbl.iter
+    (fun id decl -> 
+       try 
+	 if not decl.survive_section then
+	   decl.unfreeze_function (Stringmap.find id fs)
+       with Not_found -> decl.init_function())
+    summaries
+
 let init_summaries () =
   Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
diff --git a/library/summary.mli b/library/summary.mli
index 0d329a947..fc639d7f8 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -11,7 +11,8 @@ open Names
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit }
+  init_function : unit -> unit;
+  survive_section : bool }
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
@@ -19,6 +20,7 @@ type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
+val unfreeze_lost_summaries : frozen -> unit
 val init_summaries : unit -> unit