Supporting locality flag for custom entries + compatibility with modules.

Also prevents to use an entry name already defined.

2 files changed, 13 insertions, 7 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8455992f20..8dc2b7e139 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -564,18 +564,23 @@ let find_grammars_by_name name =
 
 let custom_entries = ref String.Map.empty
 
-let create_custom_entries s =
+let create_custom_entry local s =
+  if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
+    user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
   let sc = "constr:"^s in
   let sp = "pattern:"^s in
   let c = (Gram.entry_create sc : Constrexpr.constr_expr Gram.entry) in
   let p = (Gram.entry_create sp : Constrexpr.cases_pattern_expr Gram.entry) in
   register_grammars_by_name s [AnyEntry c; AnyEntry p];
-  custom_entries := String.Map.add s (c,p) !custom_entries
+  custom_entries := String.Map.add s (local,(c,p)) !custom_entries
 
-let find_custom_entries s =
+let lookup_custom_entry s =
   try String.Map.find s !custom_entries
   with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
 
+let find_custom_entry s = snd (lookup_custom_entry s)
+let locality_of_custom_entry s = fst (lookup_custom_entry s)
+
 (** Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
@@ -583,7 +588,7 @@ type frozen_t =
   (int * GrammarCommand.t * GramState.t) list *
   CLexer.keyword_state *
   any_entry list String.Map.t *
-  (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry) Util.String.Map.t
+  (bool * (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)) Util.String.Map.t
 
 let freeze _ : frozen_t =
   (!grammar_stack, CLexer.get_keyword_state (),
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9711cd0461..b2e1259646 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -273,7 +273,8 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
 
-(** Create a custom entry of some name *)
+(** Create a custom entry of some name; boolean is [true] if local *)
 
-val create_custom_entries : string -> unit
-val find_custom_entries : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
+val create_custom_entry : bool -> string -> unit
+val find_custom_entry : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
+val locality_of_custom_entry : string -> bool