diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 0cc869d58b98..d13cc3de4d29 100644 --- 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 index df964c9236d3..56d5698371a8 100644 --- 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 index 70de8ea84b87..39f7550ca2de 100644 --- 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