From 0c68df5ccdacb5d2ed50b533ad613723914dfee7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 24 Nov 2000 16:13:28 +0000
Subject: 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
---
 library/summary.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'library/summary.ml')

diff --git a/library/summary.ml b/library/summary.ml
index 0ba07a7374..8fbd5efe46 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
-- 
cgit v1.2.3