diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 18:57:53 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 19:09:19 +0200 |
commit | 9acfdfd9b7d1cae34b97a4c06c52c4646e15589b (patch) | |
tree | c41decbdd8bb9eb81c076cdea6d1c64bbcb0ff94 | |
parent | 16d0e6f7cfc453944874cc1665a0eb4db8ded354 (diff) |
The grammar_extend function now registers unsynchronized extensions.
This made little sense, as all the uses of this function were actually
called from toplevel ML modules. This was at best useless, and at worst
a source of bugs when loading plugins and messing with backtracking.
-rw-r--r-- | parsing/pcoq.ml | 20 | ||||
-rw-r--r-- | parsing/pcoq.mli | 23 |
2 files changed, 26 insertions, 17 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index ae56c4723..efb89cd6e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -109,11 +109,6 @@ type ext_kind = let camlp4_state = ref [] -let grammar_extend e reinit ext = - camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; - let ext = of_coq_extend_statement ext in - camlp4_verbose (maybe_uncurry (G.extend e)) ext - (** Deletion *) let grammar_delete e reinit (pos,rls) = @@ -132,6 +127,19 @@ let grammar_delete e reinit (pos,rls) = maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) | None -> () +(** Extension *) + +let grammar_extend e reinit ext = + let ext = of_coq_extend_statement ext in + let undo () = grammar_delete e reinit ext in + let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in + camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + redo () + +let grammar_extend_sync e reinit ext = + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -429,7 +437,7 @@ let extend_grammar_command tag g = | (_, _, st) :: _ -> st in let (rules, st) = modify g grammar_state in - let iter (ExtendRule (e, reinit, ext)) = grammar_extend e reinit ext in + let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in let () = List.iter iter rules in let nb = List.length rules in grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ed82607dd..319ca256e 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -96,16 +96,6 @@ module Gram : module type of Compat.GrammarMake(CLexer) *) -(** {5 Grammar extension API} *) - -(** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position - -val grammar_extend : - 'a Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - 'a Extend.extend_statment -> unit - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -232,7 +222,18 @@ val set_command_entry : vernac_expr Gram.entry -> unit val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option -(** {5 Extending the parser with Summary-synchronized commands} *) +(** {5 Extending the parser without synchronization} *) + +type gram_reinit = gram_assoc * gram_position +(** Type of reinitialization data *) + +val grammar_extend : 'a Gram.entry -> gram_reinit option -> + 'a Extend.extend_statment -> unit +(** Extend the grammar of Coq, without synchronizing it with the bactracking + mechanism. This means that grammar extensions defined this way will survive + an undo. *) + +(** {5 Extending the parser with summary-synchronized commands} *) module GramState : Store.S (** Auxilliary state of the grammar. Any added data must be marshallable. *) |