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 /parsing/pcoq.mli | |
| 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.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 23 |
1 files changed, 12 insertions, 11 deletions
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. *) |