diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 1e98722a0e0929..56ffb83a679f78 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -361,11 +361,13 @@ def findBadUnicodeAux (s : String) (pos : s.Pos) (c : Char) if ! isAllowedCharacter c then -- bad: character not allowed. findBadUnicodeAux s posₙ cₙ (err.push (.unwantedUnicode c)) - else if cₙ == UnicodeVariant.emoji && !(emojis.contains c) then + else if cₙ == UnicodeVariant.emoji && !(emojis.contains c) && !(unrestricted.contains c) then -- bad: unwanted emoji variant selector. let errₙ := err.push (.unicodeVariant (String.ofList [c, cₙ]) none) findBadUnicodeAux s posₙ cₙ errₙ - else if cₙ == UnicodeVariant.text && !(nonEmojis.contains c) then + else if + cₙ == UnicodeVariant.text && !(nonEmojis.contains c) && !(unrestricted.contains c) + then -- bad: unwanted text variant selector. let errₙ := err.push (.unicodeVariant (String.ofList [c, cₙ]) none) findBadUnicodeAux s posₙ cₙ errₙ diff --git a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean index b4b7a8b9e8c9e3..560c29f09cb792 100644 --- a/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean +++ b/Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean @@ -186,10 +186,19 @@ public def emojis : Array Char := #[ /-- Unicode symbols in mathlib that should always be followed by the text variant selector. -/ public def nonEmojis : Array Char := #[] +/-- Unicode symbols in mathlib that have no restrictions on whether they are followed by a selector +or which selector they are followed by. -/ +public def unrestricted : Array Char := #[ + '⚠' -- ⚠️, ⚠. Lake output uses '⚠' and does not include the text selector. +] + /-- If `false`, the character is not allowed in Mathlib. Implemented using an allowlist consisting of: - certain ASCII characters +- certain emojis (`emojis`) +- certain non-emoji variants of emojifiable characters (`nonEmojis`) +- certain characters with no selector restrictions (`unrestricted`) - characters with abbreviations in the VSCode extension (`withVSCodeAbbrev`) - "the rest" (`othersInMathlib`) @@ -202,6 +211,7 @@ public def isAllowedCharacter (c : Char) : Bool := || othersInMathlib.contains c || emojis.contains c || nonEmojis.contains c + || unrestricted.contains c || c == UnicodeVariant.emoji || c == UnicodeVariant.text diff --git a/MathlibTest/Linter/TextBased.lean b/MathlibTest/Linter/TextBased.lean index 1f3b696f653e86..18b54249b9caa9 100644 --- a/MathlibTest/Linter/TextBased.lean +++ b/MathlibTest/Linter/TextBased.lean @@ -665,14 +665,21 @@ open Mathlib.Linter.TextBased.UnicodeLinter /- A character either does or doesn't have an abbreviation in the VSCode extension. -/ #guard withVSCodeAbbrev.toList ∩ othersInMathlib.toList = ∅ -/- A character either is or isn't an emoji. -/ +/- No character is both an emoji and not an emoji. -/ #guard emojis.toList ∩ nonEmojis.toList = ∅ +/- No character is both an emoji and unrestricted. -/ +#guard emojis.toList ∩ unrestricted.toList = ∅ + +/- No character is both a non-emoji and unrestricted. -/ +#guard nonEmojis.toList ∩ unrestricted.toList = ∅ + def allLinterDefinedCharacterLists : List (List Char) := [ withVSCodeAbbrev, othersInMathlib, emojis, - nonEmojis + nonEmojis, + unrestricted ].map Array.toList /- Ensure none of the lists contain duplicates -/