diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 205ee6c273..1afb244f03 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1279,10 +1279,11 @@ structure ParserCategory := abbrev ParserCategories := PersistentHashMap Name ParserCategory def currLbp (left : Syntax) (c : ParserContext) (s : ParserState) : ParserState × Nat := -let (s, stx) := peekToken c s; -match stx with -| some (Syntax.atom _ sym) => - match c.tokens.matchPrefix sym 0 with +let (s, stx?) := peekToken c s; +match stx? with +| some stx@(Syntax.atom _ sym) => + if sym == "$" && checkTailNoWs stx then (s, appPrec) -- TODO: split `lbpNoWs` into "before" and "after", and set right lbp for '$' in antiquotations + else match c.tokens.matchPrefix sym 0 with | (_, some tk) => match tk.lbp, tk.lbpNoWs with | some lbp, none => (s, lbp) | none, some lbpNoWs => (s, lbpNoWs) @@ -1842,9 +1843,7 @@ let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux -- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different -- antiquotation kind via `noImmediateColon` let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP; -node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> - antiquotExpr >> - nameP >> optional "*" +node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional "*" def ident {k : ParserKind} : Parser k := mkAntiquot "ident" `ident <|> identNoAntiquot diff --git a/tests/lean/run/macro_macro.lean b/tests/lean/run/macro_macro.lean index d33ad99e6c..df866d79a8 100644 --- a/tests/lean/run/macro_macro.lean +++ b/tests/lean/run/macro_macro.lean @@ -1,6 +1,6 @@ new_frontend -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))) +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)) mk_m foo "bla" 10 'a' mk_m boo "hello" 3 'b'