Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make "Found no matching notation to enable or disable." a warning #18670

Merged
merged 1 commit into from Feb 28, 2024
Merged

Make "Found no matching notation to enable or disable." a warning #18670

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion doc/sphinx/user-extensions/syntax-extensions.rst
View file
Open in desktop
Expand Up @@ -557,7 +557,7 @@ Enabling and disabling notations
Cannot enable or disable for parsing a notation that was
originally defined as only printing.

.. exn:: Found no matching notation to enable or disable.
.. warn:: Found no matching notation to enable or disable.

No previously defined notation satisfies the given constraints.

Expand Down
8 changes: 6 additions & 2 deletions interp/notation.ml
View file
Open in desktop
Expand Up @@ -2671,6 +2671,11 @@ let toggle_abbreviations ~on found ntn_pattern =
Abbreviation.toggle_abbreviations ~on ~use:ntn_pattern.use_pattern test
with Exit -> ()

let warn_nothing_to_enable_or_disable =
CWarnings.create ~name:"no-notation-to-enable-or-disable"
~category:CWarnings.CoreCategories.syntax
(fun () -> strbrk "Found no matching notation to enable or disable.")

let toggle_notations ~on ~all ?(verbose=true) prglob ntn_pattern =
let found = ref [] in
(* Deal with (parsing) notations *)
Expand All @@ -2688,8 +2693,7 @@ let toggle_notations ~on ~all ?(verbose=true) prglob ntn_pattern =
(* Deal with abbreviations *)
toggle_abbreviations ~on found ntn_pattern;
match !found with
| [] ->
user_err (strbrk "Found no matching notation to enable or disable.")
| [] -> warn_nothing_to_enable_or_disable ()
| _::_::_ when not all ->
user_err (strbrk "More than one interpretation bound to this notation, confirm with the \"all\" modifier.")
| _ ->
Expand Down
8 changes: 5 additions & 3 deletions test-suite/output/activation.out
View file
Open in desktop
Expand Up @@ -5,12 +5,13 @@ modifier.
File "./output/activation.v", line 12, characters 0-22:
The command has indeed failed with message:
No notation provided.
File "./output/activation.v", line 15, characters 0-24:
File "./output/activation.v", line 16, characters 0-24:
The command has indeed failed with message:
Found no matching notation to enable or disable.
[no-notation-to-enable-or-disable,syntax,default]
a
: Type
File "./output/activation.v", line 24, characters 11-12:
File "./output/activation.v", line 26, characters 11-12:
The command has indeed failed with message:
The reference a was not found in the current environment.
Prop
Expand All @@ -25,6 +26,7 @@ x
: bool
0
: nat
File "./output/activation.v", line 44, characters 0-49:
File "./output/activation.v", line 47, characters 0-49:
The command has indeed failed with message:
Found no matching notation to enable or disable.
[no-notation-to-enable-or-disable,syntax,default]
4 changes: 4 additions & 0 deletions test-suite/output/activation.v
View file
Open in desktop
Expand Up @@ -12,7 +12,9 @@ Disable Notation (all) : nat_scope.
Fail Disable Notation.

Module Abbrev.
Set Warnings "+no-notation-to-enable-or-disable".
Fail Disable Notation f. (* no abbreviation with such suffix *)
Set Warnings "no-notation-to-enable-or-disable".
Notation f w := (S w).
Disable Notation f w := (S w).
Enable Notation := (S _).
Expand Down Expand Up @@ -41,6 +43,8 @@ End Abbrev.
Module Bug17782.

Declare Custom Entry trm.
Set Warnings "+no-notation-to-enable-or-disable".
Fail Disable Notation "'foo' _" (in custom trm).
Set Warnings "no-notation-to-enable-or-disable".

End Bug17782.