diff options
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | test-suite/success/custom_entry.v | 13 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 4 | ||||
| -rw-r--r-- | vernac/egramcoq.mli | 3 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 13 |
5 files changed, 32 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 734dd8ee8a..26afdcb9d5 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -533,6 +533,7 @@ let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) try EntryDataMap.find tag !camlp5_entries with Not_found -> EntryData.Ex String.Map.empty in + let () = assert (not @@ String.Map.mem name old) in let entries = String.Map.add name e old in camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries in diff --git a/test-suite/success/custom_entry.v b/test-suite/success/custom_entry.v new file mode 100644 index 0000000000..e88ae65e18 --- /dev/null +++ b/test-suite/success/custom_entry.v @@ -0,0 +1,13 @@ +Declare Custom Entry foo. + +Print Custom Grammar foo. + +Notation "[ e ]" := e (e custom foo at level 0). + +Print Custom Grammar foo. + +Notation "1" := O (in custom foo at level 0). + +Print Custom Grammar foo. + +Fail Declare Custom Entry foo. diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index b65a126f55..07656f9715 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -278,6 +278,10 @@ let find_custom_entry s = try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp) with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".") +let exists_custom_entry s = match find_custom_entry s with +| _ -> true +| exception _ -> false + let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality (* This computes the name of the level where to add a new rule *) diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index f879d51660..6768d24d5c 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -19,4 +19,7 @@ val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) val create_custom_entry : local:bool -> string -> unit + +val exists_custom_entry : string -> bool + val locality_of_custom_entry : string -> bool diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 35681aed13..222e9eb825 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1654,10 +1654,16 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing (**********************************************************************) (* Declaration of custom entry *) +let warn_custom_entry = + CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing" + (fun s -> + strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.") + let load_custom_entry _ _ = () let open_custom_entry _ (_,(local,s)) = - Egramcoq.create_custom_entry ~local s + if Egramcoq.exists_custom_entry s then warn_custom_entry s + else Egramcoq.create_custom_entry ~local s let cache_custom_entry o = load_custom_entry 1 o; @@ -1677,4 +1683,7 @@ let inCustomEntry : locality_flag * string -> obj = classify_function = classify_custom_entry} let declare_custom_entry local s = - Lib.add_anonymous_leaf (inCustomEntry (local,s)) + if Egramcoq.exists_custom_entry s then + user_err Pp.(str "Custom entry " ++ str s ++ str " already exists") + else + Lib.add_anonymous_leaf (inCustomEntry (local,s)) |