From 09ab15dc6dadc672bc35db62b4641a375830e77f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 10 Apr 2025 10:16:29 -0700 Subject: [PATCH] fix: remove infinite loop in `withFnRefWhenTagAppFns` (#7904) This PR fixes an oversight in `withFnRefWhenTagAppFns` that causes an infinite loop when the expression is a constant. This affected pretty printing of zero-field structures when `pp.tagAppFns` was true (used by docgen and verso). Closes #7898. --- .../PrettyPrinter/Delaborator/Builtins.lean | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 3b184e0575..6710eeeede 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -29,16 +29,6 @@ def withTypeAscription (d : Delab) (cond : Bool := true) : Delab := do 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. -/ @@ -134,6 +124,18 @@ def delabConst : Delab := do else return stx +/-- +If `pp.tagAppFns` is set, and if the current expression is a constant application, +then `d` is evaluated with the head constant delaborated with `delabConst` as the ref. +-/ +def withFnRefWhenTagAppFns (d : Delab) : Delab := do + if (← getExpr).getAppFn.isConst && (← getPPOption getPPTagAppFns) then + -- delabConst in `pp.tagAppFns` mode annotates the term. + let head ← withNaryFn delabConst + withRef head <| d + else + d + def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do match ← getExpr with | Expr.mdata m .. =>