From a6e7775b67fe8f82d31d16777559940d6675c94d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Oct 2019 15:41:41 +0100 Subject: Implement the unsupported attribute error using the warning system This means we can disable it to ignore unsupported attributes. For instance this would be useful if we change some behaviour of `Cmd` and add an attribute `att` to restore the old behaviour, then `#[att] Cmd` is backwards compatible if the warning is disabled. --- .../10997-unsupport-atts-warn.rst | 3 +++ doc/sphinx/language/gallina-specification-language.rst | 5 +++++ vernac/attributes.ml | 14 +++++++++----- 3 files changed, 17 insertions(+), 5 deletions(-) create mode 100644 doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + `_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ae9d284661..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1556,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 6af454eee5..b7a3b002bd 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -18,13 +18,17 @@ and vernac_flag_value = | VernacFlagLeaf of string | VernacFlagList of vernac_flags +let warn_unsupported_attributes = + CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError + (fun atts -> + let keys = List.map fst atts in + let keys = List.sort_uniq String.compare keys in + let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in + Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")) + let unsupported_attributes = function | [] -> () - | atts -> - let keys = List.map fst atts in - let keys = List.sort_uniq String.compare keys in - let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in - user_err Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".") + | atts -> warn_unsupported_attributes atts type 'a key_parser = 'a option -> vernac_flag_value -> 'a -- cgit v1.2.3