feat(Tactic/Linter): lint unwanted unicode

Mathlib/GroupTheory/GroupExtension/Defs.lean

@@ -22,14 +22,14 @@ such as splittings and equivalences.
 
 ```text
 For multiplicative groups:
-      ↗︎ E  ↘
+      ↗ E  ↘
 1 → N   ↓    G → 1
-      ↘︎ E' ↗︎️
+      ↘ E' ↗
 
 For additive groups:
-      ↗︎ E  ↘
+      ↗ E  ↘
 0 → N   ↓    G → 0
-      ↘︎ E' ↗︎️
+      ↘ E' ↗
 ```
 
 - `(Add?)GroupExtension.Splitting S`: structure for splittings of a group extension `S` of `G` by

Mathlib/Tactic/Widget/Calc.lean

@@ -116,7 +116,7 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
 @[server_rpc_method]
 def CalcPanel.rpc := mkSelectionPanelRPC suggestSteps
   "Please select subterms."
-  "Calc 🔍"
+  "Calc 🔍️"
 
 /-- The calc widget. -/
 @[widget_module]

Mathlib/Tactic/Widget/CongrM.lean

@@ -38,7 +38,7 @@ def makeCongrMString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
 @[server_rpc_method]
 def CongrMSelectionPanel.rpc := mkSelectionPanelRPC makeCongrMString
   "Use shift-click to select sub-expressions in the goal that should become holes in congrm."
-  "CongrM 🔍"
+  "CongrM 🔍️"
 
 /-- The congrm widget. -/
 @[widget_module]

Mathlib/Tactic/Widget/Conv.lean

@@ -123,7 +123,7 @@ def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
 def ConvSelectionPanel.rpc :=
 mkSelectionPanelRPC insertEnter
   "Use shift-click to select one sub-expression in the goal that you want to zoom on."
-  "Conv 🔍" (onlyGoal := false) (onlyOne := true)
+  "Conv 🔍️" (onlyGoal := false) (onlyOne := true)
 
 /-- The conv widget. -/
 @[widget_module]

Mathlib/Tactic/Widget/GCongr.lean

@@ -37,7 +37,7 @@ return (res, res, none)
 @[server_rpc_method]
 def GCongrSelectionPanel.rpc := mkSelectionPanelRPC makeGCongrString
   "Use shift-click to select sub-expressions in the goal that should become holes in gcongr."
-  "GCongr 🔍"
+  "GCongr 🔍️"
 
 /-- The gcongr widget. -/
 @[widget_module]

Mathlib/Topology/ContinuousFunction/Weierstrass.lean

@@ -69,7 +69,7 @@ theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
     rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
     -- and precomposing with an affine map takes polynomial functions to polynomial functions.
     rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p
-    -- 🎉
+    -- 🎉️
     exact p
   · -- Otherwise, `b ≤ a`, and the interval is a subsingleton,
     subsingleton [(Set.subsingleton_Icc_of_ge h).coe_sort]

test/LintStyle.lean

@@ -135,3 +135,55 @@ lemma foo' : True := trivial
 -- TODO: add terms for the term form
 
 end setOption
+
+section unicodeLinter
+
+open Mathlib.Linter.TextBased
+open Mathlib.Linter.TextBased.unicodeLinter
+
+-- test parsing back error message in `parse?_errorContext` for unicode errors
+#guard let errContext : ErrorContext := {
+    error := .unwantedUnicode '\u1234', lineNumber := 4, path:="./MYFILE.lean"}
+  (parse?_errorContext <| outputMessage errContext .exceptionsFile) == some errContext
+
+-- test parsing back error message in `parse?_errorContext` for variant selector errors
+
+-- "missing" selector
+#guard let errContext : ErrorContext := {
+    error := .unicodeVariant "\u1234A" UnicodeVariant.emoji ⟨6⟩,
+    lineNumber := 4, path:="./MYFILE.lean"}
+  (parse?_errorContext <| outputMessage errContext .exceptionsFile) == some errContext
+
+-- "wrong" selector
+#guard let errContext : ErrorContext := {
+    error := .unicodeVariant "\u1234\uFE0E" UnicodeVariant.emoji ⟨6⟩,
+    lineNumber := 4, path:="./MYFILE.lean"}
+  (parse?_errorContext <| outputMessage errContext .exceptionsFile) == some errContext
+
+-- "unexpected" selector
+#guard let errContext : ErrorContext := {
+    error := .unicodeVariant "\uFE0EA" none ⟨6⟩, lineNumber := 4, path:="./MYFILE.lean"}
+  (parse?_errorContext <| outputMessage errContext .exceptionsFile) == some errContext
+
+-- make sure hard-coded lists of unicode characters are disjoint (for clarity and maintainability)
+
+-- lists of special characters should not have allowed ASCII.
+#guard List.all [
+  othersInMathlib,
+  withVSCodeAbbrev,
+  emojis,
+  nonEmojis
+  ] fun arr ↦ arr.all (!ASCII.allowed ·)
+
+
+-- The lists of special characters should be disjoint.
+#guard othersInMathlib.toList ∩ withVSCodeAbbrev.toList = ∅
+#guard othersInMathlib.toList ∩ emojis.toList = ∅
+#guard othersInMathlib.toList ∩ nonEmojis.toList = ∅
+
+#guard withVSCodeAbbrev.toList ∩ emojis.toList = ∅
+#guard withVSCodeAbbrev.toList ∩ nonEmojis.toList = ∅
+
+#guard emojis.toList ∩ nonEmojis.toList = ∅
+
+end unicodeLinter