diff options
| author | Pierre-Marie Pédrot | 2019-12-19 18:03:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-22 14:04:01 +0100 |
| commit | fcd903c299db00d5c8d3e2fa797404eb880b61ac (patch) | |
| tree | d1d339cb530d2f8e0c4afd11f49fb810383eb5ec /vernac | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
Ensure that a custom entry cannot be defined twice.
This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 4 | ||||
| -rw-r--r-- | vernac/egramcoq.mli | 3 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 13 |
3 files changed, 18 insertions, 2 deletions
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)) |