From 9acfdfd9b7d1cae34b97a4c06c52c4646e15589b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 11 May 2016 18:57:53 +0200
Subject: 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.
---
 parsing/pcoq.ml  | 20 ++++++++++++++------
 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. *)
-- 
cgit v1.2.3