feat: elaborate syntaxAbbrev as a definition

@Kha I elaborated it as a definition. It works because we can now
reference Parser declarations in `syntax` command.
This change allowed us to replace `p.getArg 0` with `p` in the
`Websever` demo.

src/Lean/Elab/Syntax.lean

@@ -236,6 +236,16 @@ fun stx => do
   trace `Elab stx $ fun _ => d;
   withMacroExpansion stx d $ elabCommand d
 
+/-
+def syntaxAbbrev  := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
+-/
+@[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab :=
+fun stx => do
+  let declName := stx.getArg 1;
+  (val, _) ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 3) Name.anonymous;
+  stx' ← `(def $declName : Lean.ParserDescr := $val);
+  withMacroExpansion stx stx' $ elabCommand stx'
+
 def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
 alts ← alts.mapSepElemsM $ fun alt => do {
   let lhs := alt.getArg 0;

tests/playground/webserver/Webserver.lean

@@ -78,13 +78,6 @@ open Lean
 namespace Prelim
 open Lean.Parser
 
--- for declaring simple parsers I can still use within other `syntax`
-@[commandParser] def syntaxAbbrev := parser! symbol "syntax " >> ident >> symbol " := " >> many1 syntaxParser
-@[macro Prelim.syntaxAbbrev] def elabSyntaxAbbrev : Macro :=
-fun stx => match_syntax stx with
-| `(syntax $id := $p*) => `(declare_syntax_cat $id  syntax:0 $p* : $id)
-| _ => Macro.throwUnsupported
-
 -- "JSXTextCharacter : SourceCharacter but not one of {, <, > or }"
 def text : Parser := {
   fn := fun c s =>
@@ -155,7 +148,7 @@ syntax "POST" : verb
 
 macro v:verb p:path " => " t:term : command => do
   t ← `(do checkPathConsumed; $t:term);
-  t ← (p.getArg 0).getArgs.foldrM (fun pi t => match_syntax pi with
+  t ← p.getArgs.foldrM (fun pi t => match_syntax pi with
     | `(pathItem|$l:pathLiteral) => `(do checkPathLiteral $(mkStxStrLit (l.getArg 0).getAtomVal!); $t:term)
     | `(pathItem|{$id}) => `(do $id:ident ← getPathPart; $t:term)
     | _ => unreachable!) t;