From 8aab74e65d21b7a2d783ea99d27d0fe47ab01c54 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 15 Feb 2024 09:40:54 -0800 Subject: [PATCH] fix: make `withOverApp` annotate the expression position and register `TermInfo` (#3327) This makes it so that when `withOverApp` is handling overapplied functions, the term produced by the supplied delaborator is hoverable in the Infoview. --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 11 +++++++++++ src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 8 ++++++-- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 576a84dd90..e282f0ef53 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -269,11 +269,22 @@ def shouldOmitExpr (e : Expr) : DelabM Bool := do return depthExcess > 0 && !isShallowExpression +/-- +Annotates the term with the current expression position and registers `TermInfo` +to associate the term to the current expression. +-/ def annotateTermInfo (stx : Term) : Delab := do let stx ← annotateCurPos stx addTermInfo (← getPos) stx (← getExpr) pure stx +/-- +Modifies the delaborator so that it annotates the resulting term with the current expression +position and registers `TermInfo` to associate the term to the current expression. +-/ +def withAnnotateTermInfo (d : Delab) : Delab := do + let stx ← d + annotateTermInfo stx /-- Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index d5e17b7483..a9419494aa 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -331,7 +331,11 @@ With this combinator one can use an arity-2 delaborator to pretty print this as The combinator will fail if fewer than this number of arguments are passed, and if more than this number of arguments are passed the arguments are handled using the standard application delaborator. -* `x`: constructs data corresponding to the main application (`f x` in the example) +* `x`: constructs data corresponding to the main application (`f x` in the example). + +In the event of overapplication, the delaborator `x` is wrapped in +`Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo` to register `TermInfo` for the resulting term. +The effect of this is that the term is hoverable in the Infoview. -/ def withOverApp (arity : Nat) (x : Delab) : Delab := do let n := (← getExpr).getAppNumArgs @@ -339,7 +343,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do if n == arity then x else - delabAppCore (n - arity) x + delabAppCore (n - arity) (withAnnotateTermInfo x) /-- State for `delabAppMatch` and helpers. -/ structure AppMatchState where