chore: remove weird syntax sugar from macro command

Before this commit,
```
macro term x:term : term => `($x)
```
would generate the notation
```
syntax "term" term : term
```

src/Lean/Elab/Syntax.lean

@@ -505,15 +505,6 @@ def expandMacroArgIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
   else
     Macro.throwUnsupported
 
-/- Convert `macro` head into a `syntax` command item -/
-def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
-  if stx.isIdent then
-    let info := stx.getHeadInfo.getD {}
-    let id   := stx.getId
-    pure $ Syntax.node `Lean.Parser.Syntax.atom #[Syntax.mkStrLit (toString id) info]
-  else
-    expandMacroArgIntoSyntaxItem stx
-
 /- Convert `macro` arg into a pattern element -/
 def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
   let k := stx.getKind
@@ -525,13 +516,6 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
   else
     Macro.throwUnsupported
 
-/- Convert `macro` head into a pattern element -/
-def expandMacroHeadIntoPattern (stx : Syntax) : MacroM Syntax :=
-  if stx.isIdent then
-    pure $ mkAtomFrom stx (toString stx.getId)
-  else
-    expandMacroArgIntoPattern stx
-
 def expandOptPrio (stx : Syntax) : Nat :=
   if stx.isNone then
     0
@@ -545,13 +529,13 @@ def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := d
   let args := stx[4].getArgs
   let cat  := stx[6]
   -- build parser
-  let stxPart  ← liftMacroM <| expandMacroHeadIntoSyntaxItem head
+  let stxPart  ← liftMacroM <| expandMacroArgIntoSyntaxItem head
   let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem
   let stxParts := #[stxPart] ++ stxParts
   -- kind
   let kind ← mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
   -- build macro rules
-  let patHead ← liftMacroM <| expandMacroHeadIntoPattern head
+  let patHead ← liftMacroM <| expandMacroArgIntoPattern head
   let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
@@ -595,13 +579,13 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
   let rhs     := stx[9]
   let catName := cat.getId
   -- build parser
-  let stxPart  ← liftMacroM <| expandMacroHeadIntoSyntaxItem head
+  let stxPart  ← liftMacroM <| expandMacroArgIntoSyntaxItem head
   let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem
   let stxParts := #[stxPart] ++ stxParts
   -- kind
   let kind ← mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
   -- build pattern for `martch_syntax
-  let patHead ← liftMacroM <| expandMacroHeadIntoPattern head
+  let patHead ← liftMacroM <| expandMacroArgIntoPattern head
   let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
   let pat := Syntax.node (currNamespace ++ kind) (#[patHead] ++ patArgs)
   let kindId    := mkIdentFrom ref kind

src/Lean/Parser/Syntax.lean

@@ -69,7 +69,7 @@ def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|>
 @[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
 def macroArg  := strLit <|> atomic macroArgSimple
-def macroHead := macroArg <|> ident
+def macroHead := macroArg
 def macroTailTactic   : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
 def macroTailCommand  : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
 def macroTailDefault  : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)

tests/lean/macroStack.lean

@@ -1,4 +1,4 @@
-
+--
 
 def f1 :=
 if h:x then 1 else 0
@@ -10,8 +10,8 @@ if h:(x > 0) then 1 else 0
 
 def x := <- get
 
-macro foo! x:term:max : term => `(let x := "hello"; $x + x)
-macro bla! x:term:max : term => `(fun (x : Nat) => if foo! ($x + x) < 1 then true else false)
+macro "foo!" x:term:max : term => `(let x := "hello"; $x + x)
+macro "bla!" x:term:max : term => `(fun (x : Nat) => if foo! ($x + x) < 1 then true else false)
 
 def f (x : Nat) :=
 bla! x

tests/lean/namelit.lean

@@ -1,4 +1,4 @@
-
+--
 
 #check `foo
 #check `foo.bla
@@ -7,8 +7,8 @@
 #check `«foo bla».boo.«hello world»
 #check `foo.«hello»
 
-macro dummy1 : term => `(`hello)
-macro dummy2 : term => `(`hello.«world !!!»)
+macro "dummy1" : term => `(`hello)
+macro "dummy2" : term => `(`hello.«world !!!»)
 
 #check dummy1
 #check dummy2

tests/lean/run/108.lean

@@ -1,6 +1,4 @@
-
-
-macro m n:ident : command => `(def $n := 1)
+macro "m" n:ident : command => `(def $n := 1)
 
 m foo
 

tests/lean/run/extmacro.lean

@@ -1,6 +1,4 @@
-
-
-macro ext_tactic t:tactic "=>" newT:tactic : command => `(macro_rules | `($t) => `($newT))
+macro "ext_tactic" t:tactic "=>" newT:tactic : command => `(macro_rules | `($t) => `($newT))
 
 syntax "trivial" : tactic
 

tests/lean/run/macro_macro.lean

@@ -1,6 +1,8 @@
+macro "mk_m " id:ident v:str n:num c:char : command =>
+  let tk : Lean.Syntax := Lean.Syntax.mkStrLit id.getId.toString
+  `(macro $tk:strLit : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c))
 
-
-macro mk_m id:ident v:str n:num c:char : command => `(macro $id:ident : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c))
+#print " ---- "
 
 mk_m foo "bla" 10 'a'
 mk_m boo "hello" 3 'b'

tests/lean/run/newfrontend1.lean

@@ -63,9 +63,9 @@ by {
   assumption
 }
 
-macro intro3 : tactic => `(intro; intro; intro)
-macro check2 x:term : command => `(#check $x #check $x)
-macro foo x:term "," y:term : term => `($x + $y + $x)
+macro "intro3" : tactic => `(intro; intro; intro)
+macro "check2" x:term : command => `(#check $x #check $x)
+macro "foo" x:term "," y:term : term => `($x + $y + $x)
 
 set_option pp.all false
 

tests/lean/weirdmacro.lean

@@ -0,0 +1,4 @@
+macro term x:term : term => `($x)
+
+#check term 10
+-- 10

tests/lean/weirdmacro.lean.expected.out

@@ -0,0 +1,4 @@
+weirdmacro.lean:1:6: error: expected no space before ':' or string literal
+weirdmacro.lean:1:30: error: elaboration function for 'antiquot' has not been implemented
+weirdmacro.lean:1:32: error: expected term
+weirdmacro.lean:3:7: error: unknown identifier 'term'