feat: mkAntiquotNode

src/Lean/Elab/Quotation.lean

@@ -15,6 +15,19 @@ namespace Lean.Elab.Term.Quotation
 open Lean.Syntax (isQuot isAntiquot)
 open Meta
 
+def mkAntiquotNode (term : Syntax) (nesting := 0) (name : Option String := none) (kind := Name.anonymous) (splice := false) : Syntax :=
+  let nesting := mkNullNode (mkArray nesting (mkAtom "$"))
+  let term := match term.isIdent with
+    | true  => term
+    | false => mkNode `antiquotNestedExpr #[mkAtom "(", term, mkAtom ")"]
+  let name := match name with
+    | some name => mkNode `antiquotName #[mkAtom ":", mkAtom name]
+    | none      => mkNullNode
+  let splice := match splice with
+    | true  => mkNullNode #[mkAtom "*"]
+    | false => mkNullNode
+  mkNode (kind ++ `antiquot) #[mkAtom "$", nesting, term, name, splice]
+
 -- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros.
 def isEscapedAntiquot (stx : Syntax) : Bool :=
   !stx[1].getArgs.isEmpty

src/Lean/Elab/Syntax.lean

@@ -164,6 +164,7 @@ def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Syntax × Bool) :
 end Term
 
 namespace Command
+open Term.Quotation (mkAntiquotNode)
 
 private def getCatSuffix (catName : Name) : String :=
   match catName with
@@ -344,7 +345,7 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
   | stx => match_syntax stx with
   | `($id:ident) =>
     if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
-      Syntax.node `antiquot #[mkAtom "$", mkNullNode, id, mkNullNode, mkNullNode]
+      mkAntiquotNode id
     else
       stx
   | _ => match stx with
@@ -370,8 +371,7 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
 def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
   let k := stx.getKind
   if k == `Lean.Parser.Command.identPrec then
-    let item := stx[0]
-    pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
+    mkAntiquotNode stx[0]
   else if k == strLitKind then
     strLitToPattern stx
   else