withHeadRefIfTagAppFns — Mathlib

Lean4
/-- If `pp.tagAppFns` is true and the head of the current expression is a constant,
then delaborates the head and uses it for the ref.
This causes tokens inside the syntax to refer to this constant.
A consequence is that docgen will linkify the tokens.
-/
def withHeadRefIfTagAppFns (d : Delab) : Delab := do
  let tagAppFns ← getPPOption getPPTagAppFns
  if tagAppFns && (← getExpr).getAppFn.consumeMData.isConst then
      -- Delaborate the head to register term info and get a syntax we can use for the ref.
          -- The syntax `f` itself is thrown away.

    let f ← withNaryFn <| withOptionAtCurrPos `pp.tagAppFns true delab
    let stx ← withRef f d
    annotateTermInfo stx
  else
    d
Похожие утверждения