diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:18 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:18 +0000 |
| commit | a672da543ac5ba589abb016e8f1cd8e448326fc3 (patch) | |
| tree | 555afbb2fd4b3b1c4dca2d63f987c7e51bbcac51 | |
| parent | 85dd53ed83f229044f2b19a9ef46387ff981aa57 (diff) | |
Egramcoq+Lexer : no need for an init_function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16448 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/egramcoq.ml | 12 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 9 | ||||
| -rw-r--r-- | parsing/lexer.mli | 1 |
3 files changed, 6 insertions, 16 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 1b1c7dafd..c10516839 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -325,18 +325,16 @@ let unfreeze (grams, lex) = Lexer.unfreeze lex; List.iter extend_grammar (List.rev_map snd redo) -let init_grammar () = - remove_grammars (number_of_entries !grammar_state); - grammar_state := [] - -let init () = - init_grammar () +(** No need to provide an init function : the grammar state is + statically available, and already empty initially, while + the lexer state should not be resetted, since it contains + keywords declared in g_*.ml4 *) let _ = Summary.declare_summary "GRAMMAR_LEXER" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = Summary.nop } let with_grammar_rule_protection f x = let fs = freeze () in diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 91e7846dc..bf30d9d35 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -231,14 +231,7 @@ let remove_keyword str = type frozen_t = ttree let freeze () = !token_tree - -let unfreeze tt = - token_tree := tt - -let init () = - unfreeze empty_ttree - -let _ = init() +let unfreeze tt = (token_tree := tt) (* The string buffering machinery *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 0e53bd615..cef53a871 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -26,7 +26,6 @@ val check_keyword : string -> unit type frozen_t val freeze : unit -> frozen_t val unfreeze : frozen_t -> unit -val init : unit -> unit type com_state val com_state: unit -> com_state |