diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 22cc9f8121..3ed39ff4c8 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/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; diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean index 904094b095..8041d34a2d 100644 --- a/tests/playground/webserver/Webserver.lean +++ b/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;