From 7ec23f9401aef154d7b797f06d39ea2ebc2f0152 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Jun 2020 13:54:50 -0700
Subject: [PATCH] fix: `macro` command syntax

---
 src/Lean/Elab/Syntax.lean   | 6 +++---
 src/Lean/Parser/Syntax.lean | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 1096040ce8..9eb9c9f663 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -375,7 +375,7 @@ else
 
 @[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro :=
 fun stx => do
-  let prec := stx.getArg 1;
+  let prec := (stx.getArg 1).getArgs;
   let head := stx.getArg 2;
   let args := (stx.getArg 3).getArgs;
   let cat  := stx.getArg 5;
@@ -391,11 +391,11 @@ fun stx => do
   if stx.getArgs.size == 8 then
     -- `stx` is of the form `macro $head $args* : $cat => term`
     let rhs := stx.getArg 7;
-    `(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
+    `(syntax $prec* [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
   else
     -- `stx` is of the form `macro $head $args* : $cat => `( $body )`
     let rhsBody := stx.getArg 8;
-    `(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
+    `(syntax $prec* [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.syntax;
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 4c08be987d..ebdc3708fc 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -64,7 +64,7 @@ def optKind : Parser := optional ("[" >> ident >> "]")
 @[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts
 @[builtinCommandParser] def «syntax»      := parser! "syntax " >> optPrecedence >> optKind >> many1 syntaxParser >> " : " >> ident
 @[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident
-def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> ident
+def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> (ident >> optPrecedence)
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
 def macroArg  := try strLit <|> try macroArgSimple
 def macroHead := macroArg <|> try ident