feat: modify delaborator to tag generalized field notation (leanprover#6703)

This PR modifies the delaborator so that in `pp.tagAppFns` mode,
generalized field notation is tagged with the head constant. The effect
is that docgen documentation will linkify dot notation. Internal change:
now formatted `rawIdent` can be tagged.

Author: kmill

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -427,7 +427,7 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
         let isFirst := args[0:fieldIdx].all (· matches .skip)
         -- Clear the `obj` argument from `args`.
         let args' := args.set! fieldIdx .skip
-        let mut head : Term ← `($obj.$(mkIdent field))
+        let mut head : Term ← `($obj.$(mkIdentFrom fnStx field))
         if isFirst then
           -- If the object is the first argument (after some implicit arguments),
           -- we can annotate `obj.field` with the prefix of the application

src/Lean/PrettyPrinter/Formatter.lean

@@ -441,9 +441,9 @@ def identNoAntiquot.formatter : Formatter := do
 
 @[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
   checkKind identKind
-  let Syntax.ident info _ id _ ← getCur
+  let stx@(Syntax.ident info _ id _) ← getCur
     | throwError m!"not an ident: {← getCur}"
-  pushToken info id.toString true
+  withMaybeTag (getExprPos? stx) (pushToken info id.toString true)
   goLeft
 
 @[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter