diff options
| -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 ae56c4723b..efb89cd6e1 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 ed82607dd2..319ca256e1 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. *) |