Merge PR #13530: Revert removal of eoi_entry in #13447

Reviewed-by: herbelin

4 files changed, 21 insertions, 1 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index a482e044d8..cc9e1bb31d 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -175,7 +175,21 @@ let rec remove_grammars n =
            camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries;
            remove_grammars (n - 1)
 
-(* Parse a string, does NOT check if the entire string was read *)
+let make_rule r = [None, None, r]
+
+(** An entry that checks we reached the end of the input. *)
+
+(* used by the Tactician plugin *)
+let eoi_entry en =
+  let e = Entry.make ((Entry.name en) ^ "_eoi") in
+  let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (Symbol.token Tok.PEOI) in
+  let act = fun _ x loc -> x in
+  let ext = { pos = None; data = make_rule [Production.make symbs act] } in
+  safe_extend e ext;
+  e
+
+(* Parse a string, does NOT check if the entire string was read
+   (use eoi_entry) *)
 
 let parse_string f ?loc x =
   let strm = Stream.of_string x in
@@ -289,6 +303,7 @@ module Constr =
     let constr = Entry.create "constr"
     let term = Entry.create "term"
     let operconstr = term
+    let constr_eoi = eoi_entry constr
     let lconstr = Entry.create "lconstr"
     let binder_constr = Entry.create "binder_constr"
     let ident = Entry.create "ident"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8bff5cfd94..06d05a4797 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -120,6 +120,7 @@ end
 (** Parse a string *)
 
 val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
+val eoi_entry : 'a Entry.t -> 'a Entry.t
 
 type gram_universe [@@deprecated "Deprecated in 8.13"]
 [@@@ocaml.warning "-3"]
@@ -180,6 +181,7 @@ module Prim :
 module Constr :
   sig
     val constr : constr_expr Entry.t
+    val constr_eoi : constr_expr Entry.t
     val lconstr : constr_expr Entry.t
     val binder_constr : constr_expr Entry.t
     val term : constr_expr Entry.t
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 80c13a3698..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -47,6 +47,8 @@ let binder_tactic = Entry.create "binder_tactic"
 let tactic = Entry.create "tactic"
 
 (* Main entry for quotations *)
+let tactic_eoi = eoi_entry tactic
+
 let () =
   let open Stdarg in
   let open Tacarg in
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 73bce84d18..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -40,3 +40,4 @@ val tactic_expr : raw_tactic_expr Entry.t
   [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
 val binder_tactic : raw_tactic_expr Entry.t
 val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t