From 8ebe0cb94fd4fed1a5358f88b274cf026e59a652 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 26 Dec 2019 18:49:26 +0100
Subject: [PATCH] feat: fieldIdx antiquotation

---
 src/Init/Lean/Parser/Parser.lean | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 316cae3a7d..0b7450c705 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1098,20 +1098,6 @@ fun _ c s =>
 def unquotedSymbol {k : ParserKind} : Parser k :=
 { fn := unquotedSymbolFn }
 
-def fieldIdxFn : BasicParserFn :=
-fun c s =>
-  let iniPos := s.pos;
-  let curr     := c.input.get iniPos;
-  if curr.isDigit && curr != '0' then
-    let s     := takeWhileFn (fun c => c.isDigit) c s;
-    mkNodeToken fieldIdxKind iniPos c s
-  else
-    s.mkErrorAt "field index" iniPos
-
-@[inline] def fieldIdx {k : ParserKind} : Parser k :=
-{ fn   := fun _ => fieldIdxFn,
-  info := mkAtomicInfo "fieldIdx" }
-
 instance string2basic {k : ParserKind} : HasCoe String (Parser k) :=
 ⟨symbolAux⟩
 
@@ -1576,6 +1562,21 @@ node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> termParse
 def ident {k : ParserKind} : Parser k :=
 mkAntiquot "ident" `ident <|> identNoAntiquot
 
+def fieldIdxFn : BasicParserFn :=
+fun c s =>
+  let iniPos := s.pos;
+  let curr     := c.input.get iniPos;
+  if curr.isDigit && curr != '0' then
+    let s     := takeWhileFn (fun c => c.isDigit) c s;
+    mkNodeToken fieldIdxKind iniPos c s
+  else
+    s.mkErrorAt "field index" iniPos
+
+@[inline] def fieldIdx {k : ParserKind} : Parser k :=
+mkAntiquot "fieldIdx" `fieldIdx <|>
+{ fn   := fun _ => fieldIdxFn,
+  info := mkAtomicInfo "fieldIdx" }
+
 end Parser
 
 namespace Syntax