From cd0b54ce5d7c018a79517fef38cf3f2f9134e96d Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 6 Apr 2025 22:07:05 -0700
Subject: [PATCH] feat: tag structure instances when `pp.tagAppFn` is set
 (#7840)

This PR causes structure instance notation to be tagged with the
constructor when `pp.tagAppFns` is true. This will make docgen will have
`{` and `}` be links to the structure constructor.
---
 .../PrettyPrinter/Delaborator/Builtins.lean    | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index d5f4eb7d5b..3b184e0575 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -20,15 +20,25 @@ open TSyntax.Compat
 /--
 If `cond` is true, wraps the syntax produced by `d` in a type ascription.
 -/
-def withTypeAscription (d : Delab) (cond : Bool := true) : DelabM Term := do
+def withTypeAscription (d : Delab) (cond : Bool := true) : Delab := do
   let stx ← d
   if cond then
-    let stx ← annotateCurPos stx
+    let stx ← annotateTermInfoUnlessAnnotated stx
     let typeStx ← withType delab
     `(($stx : $typeStx))
   else
     return stx
 
+/--
+If `pp.tagAppFns` is set, then `d` is evaluated with the delaborated head constant as the ref.
+-/
+def withFnRefWhenTagAppFns (d : Delab) : Delab := do
+  if (← getExpr).getAppFn.isConst && (← getPPOption getPPTagAppFns) then
+    let head ← withNaryFn delab
+    withRef head <| d
+  else
+    d
+
 /--
 Wraps the identifier (or identifier with explicit universe levels) with `@` if `pp.analysis.blockImplicit` is set to true.
 -/
@@ -637,7 +647,7 @@ def delabStructureInstance : Delab := do
         else
           return (i + 1, args))
     withTypeAscription (cond := (← withType <| getPPOption getPPStructureInstanceType)) do
-      `(⟨$[$args],*⟩)
+      withFnRefWhenTagAppFns `(⟨$[$args],*⟩)
   else
     /-
     Otherwise, we use structure instance notation.
@@ -650,7 +660,7 @@ def delabStructureInstance : Delab := do
     let (_, fields) ← collectStructFields s.induct levels params #[] {} s
     let tyStx? : Option Term ← withType do
       if ← getPPOption getPPStructureInstanceType then delab else pure none
-    `({ $fields,* $[: $tyStx?]? })
+    withFnRefWhenTagAppFns `({ $fields,* $[: $tyStx?]? })
 
 
 /-- State for `delabAppMatch` and helpers. -/