From f20d4aaa834fc7a079826ddefcc773ee7036a97e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jan 2020 10:19:16 -0800
Subject: [PATCH] fix: avoid `termParser` at `mkAntiquot`

@kha `mkAntiquot` is used in all categories. I removed
`termParser (appPrec + 1)` to avoid nasty interactions between
`termParser` and the surrounding category.
This commity ensures the antiquotation prefix is one of the following
forms `$<id>` or `$(<term>)`.
I made the two cases look like term syntax because I didn't want to
change your expander. We should fix this next week.
---
 src/Init/Lean/Parser/Parser.lean | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index bea55d2dd4..205ee6c273 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1821,6 +1821,16 @@ private def noImmediateColon {k : ParserKind} : Parser k :=
 private def pushNone {k : ParserKind} : Parser k :=
 { fn := fun a c s => s.pushSyntax mkNullNode }
 
+/-
+  We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
+
+  TODO: we are making both cases look like syntax terms. Reason: the current expander expects a term.
+  We should remove this hack and modify the expander. This hack is bad since it relies on how we define `id` and `paren` in
+  the term parser at `Term.lean`. -/
+private def antiquotId {k} : Parser k         := node `Lean.Parser.Term.id (identNoAntiquot >> pushNone)
+private def antiquotNestedExpr {k} : Parser k := node `Lean.Parser.Term.paren ("(" >> node nullKind (termParser >> pushNone) >> ")")
+private def antiquotExpr {k} : Parser k       := antiquotId <|> antiquotNestedExpr
+
 /--
   Define parser for `$e` (if anonymous == true) and `$e:name`. Both
   forms can also be used with an appended `*` to turn them into an
@@ -1833,8 +1843,7 @@ let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux
 -- antiquotation kind via `noImmediateColon`
 let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
 node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >>
-  -- use high precedence so that `$(x).y` is parsed as a projection of an antiquotation
-  termParser (appPrec + 1) >>
+  antiquotExpr >>
   nameP >> optional "*"
 
 def ident {k : ParserKind} : Parser k :=