diff options
| author | gareuselesinge | 2013-05-06 13:40:58 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-05-06 13:40:58 +0000 |
| commit | 9fa14555270fa8f2368a7f4df1510bd2937d25ec (patch) | |
| tree | 5ca417f25ef2f0c2425820494f0a097b12f82b50 /parsing | |
| parent | 683afb998ceb8302f3d9ec1d69cfe1ee86816c13 (diff) | |
States: frozen states can hold closures
States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values. The flag is propagated to Lib and Summary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index c105168399..9905a5ad4d 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -306,7 +306,7 @@ let recover_notation_grammar ntn prec = grammar rules. *) type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t -let freeze () : frozen_t = (!grammar_state, Lexer.freeze ()) +let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) @@ -337,7 +337,7 @@ let _ = Summary.init_function = Summary.nop } let with_grammar_rule_protection f x = - let fs = freeze () in + let fs = freeze false in try let a = f x in unfreeze fs; a with reraise -> let reraise = Errors.push reraise in |