From c6100ed25f2e094b6aae493ed8dd29ebefca1c91 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 6 Jan 2020 21:57:01 +0100
Subject: [PATCH] feat: antiquoting rawIdent

---
 src/Init/Lean/Parser/Parser.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 4fa4fc26bd..f209ee5c14 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1069,7 +1069,7 @@ fun _ c s =>
 { fn   := identFn,
   info := mkAtomicInfo "ident" }
 
-@[inline] def rawIdent {k : ParserKind} : Parser k :=
+@[inline] def rawIdentNoAntiquot {k : ParserKind} : Parser k :=
 { fn := fun _ => rawIdentFn }
 
 def quotedSymbolFn {k : ParserKind} : ParserFn k :=
@@ -1755,6 +1755,10 @@ node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >>
 def ident {k : ParserKind} : Parser k :=
 mkAntiquot "ident" `ident <|> identNoAntiquot
 
+-- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
+def rawIdent {k : ParserKind} : Parser k :=
+mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
+
 def fieldIdxFn : BasicParserFn :=
 fun c s =>
   let iniPos := s.pos;