diff options
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 *) |