fix: validate atoms modulo leading and trailing whitespace

Closes #6011
leanprover · Nov 8, 2024 · 2c372e9 · 2c372e9
1 parent c779f3a
commit 2c372e9
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
@@ -242,7 +242,7 @@ where
   processAtom (stx : Syntax) := do
     match stx[0].isStrLit? with
     | some atom =>
-      unless isValidAtom atom do
+      unless isValidAtom atom.trim do
         throwErrorAt stx "invalid atom"
       /- For syntax categories where initialized with `LeadingIdentBehavior` different from default (e.g., `tactic`), we automatically mark
          the first symbol as nonReserved. -/

diff --git a/tests/lean/242.lean b/tests/lean/242.lean
@@ -2,3 +2,7 @@ syntax "0" : term
 syntax "'a'" : term
 syntax "`a" : term
 syntax "\"a" : term
+syntax " 0" : term
+syntax " 'a'" : term
+syntax " `a" : term
+syntax " \"a" : term
diff --git a/tests/lean/242.lean.expected.out b/tests/lean/242.lean.expected.out
@@ -2,3 +2,7 @@
 242.lean:2:7-2:12: error: invalid atom
 242.lean:3:7-3:11: error: invalid atom
 242.lean:4:7-4:12: error: invalid atom
+242.lean:5:7-5:11: error: invalid atom
+242.lean:6:7-6:13: error: invalid atom
+242.lean:7:7-7:12: error: invalid atom
+242.lean:8:7-8:13: error: invalid atom