fix: validate atoms modulo leading and trailing whitespace (#6012)

This PR improves the validation of new syntactic tokens. Previously, the
validation code had inconsistencies: some atoms would be accepted only
if they had a leading space as a pretty printer hint. Additionally,
atoms with internal whitespace are no longer allowed.

Closes #6011

src/Lean/Elab/Syntax.lean

@@ -233,11 +233,14 @@ where
     return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy1) $p $sep $psep $(quote allowTrailingSep)), 1)
 
   isValidAtom (s : String) : Bool :=
+    -- Pretty-printing instructions shouldn't affect validity
+    let s := s.trim
     !s.isEmpty &&
-    s.front != '\'' &&
+    (s.front != '\'' || s == "''") &&
     s.front != '\"' &&
     !(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
-    !s.front.isDigit
+    !s.front.isDigit &&
+    !(s.any Char.isWhitespace)
 
   processAtom (stx : Syntax) := do
     match stx[0].isStrLit? with

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

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

tests/lean/run/utf8英語.lean

@@ -15,7 +15,7 @@ def checkGet (s : String) (arr : Array UInt8) :=
     let c := if h : _ then s.getUtf8Byte i h else unreachable!
     c == arr.get! i
 
-macro "validate" arr:term " => ↯" : command =>
+macro "validate" arr:term " => " "↯" : command =>
   `(test_extern' String.validateUTF8 $arr => false)
 macro "validate" arr:term " => " str:term : command =>
   `(test_extern' String.validateUTF8 $arr => true