diff options
| author | filliatr | 2000-11-24 16:13:28 +0000 |
|---|---|---|
| committer | filliatr | 2000-11-24 16:13:28 +0000 |
| commit | 0c68df5ccdacb5d2ed50b533ad613723914dfee7 (patch) | |
| tree | c83306fc05e7f70bdcd756086368e04b32e2699b /toplevel | |
| parent | 7f40f2807d4046a7cea8e83cb0a983cdc6401f78 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 3 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 6 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 3 |
3 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6e79134bb9..2b552fffc0 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -290,13 +290,14 @@ and module_contents seg = let close_section _ s = let oldenv = Global.env() in - let process_segment sec_sp decls = + let process_segment fs sec_sp decls = let newdir = dirpath sec_sp in let olddir = wd_of_sp sec_sp in let (ops,ids,_) = List.fold_left (process_item oldenv newdir olddir) ([],[],([],[],[])) decls in + Summary.unfreeze_lost_summaries fs; Global.pop_named_decls ids; List.iter process_operation (List.rev ops); module_contents decls diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index eb7543f3dd..0597238cd8 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -38,7 +38,8 @@ let _ = declare_summary "syntax" { freeze_function = Esyntax.freeze; unfreeze_function = Esyntax.unfreeze; - init_function = Esyntax.init } + init_function = Esyntax.init; + survive_section = false } (* Pretty-printing objects = syntax_entry *) let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj @@ -69,7 +70,8 @@ let _ = declare_summary "GRAMMAR_LEXER" { freeze_function = Egrammar.freeze; unfreeze_function = Egrammar.unfreeze; - init_function = Egrammar.init} + init_function = Egrammar.init; + survive_section = false } (* Tokens *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index f255739b30..0c81359cbf 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -200,7 +200,8 @@ let _ = Summary.declare_summary "ML-MODULES" { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); - Summary.init_function = (fun () -> init_ml_modules ()) } + Summary.init_function = (fun () -> init_ml_modules ()); + Summary.survive_section = true } (* Same as restore_ml_modules, but verbosely *) |