From ce5814043bb9a81be2e7407114d8b435dba1f2aa Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 17 May 2026 06:39:49 -0700
Subject: [PATCH] feat: add `MessageData.withExprHover` (#13763)

This PR adds `MessageData.withExprHover`, for creating messages that
show information about an expression when hovered over. A
`withExprHoverM` variant captures the current local context.
---
 src/Lean/Elab/Tactic/Doc.lean | 12 +---------
 src/Lean/Message.lean         | 41 +++++++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean
index ad5b6c4347..7cf39d3158 100644
--- a/src/Lean/Elab/Tactic/Doc.lean
+++ b/src/Lean/Elab/Tactic/Doc.lean
@@ -90,17 +90,7 @@ private def showParserName [Monad m] [MonadEnv m] (firsts : NameMap String) (n :
     env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
 
   let tok := ((← customTacticName n) <|> firsts.get? n).map Std.Format.text |>.getD (format n)
-  pure <| .ofFormatWithInfos {
-    fmt := "`" ++ .tag 0 tok ++ "`",
-    infos :=
-      .ofList [(0, .ofTermInfo {
-        lctx := .empty,
-        expr := .const n params,
-        stx := .ident .none (toString n).toRawSubstring n [.decl n []],
-        elaborator := `Delab,
-        expectedType? := none
-      })] _
-  }
+  pure m!"`{.withExprHover tok (.const n params) {}}`"
 
 /--
 Displays all available tactic tags, with documentation.
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index d5552f455c..db099029ce 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -275,6 +275,47 @@ def ofConstName (constName : Name) (fullNames : Bool := false) : MessageData :=
       return Dynamic.mk msg)
     (fun _ => false)
 
+/--
+Creates message data wrapping `fmt` that gives information about `expr` when hovered over.
+
+Options:
+- `location?` overrides what "go to definition" does
+- `docString?` allows overriding the docstring for the expression
+- `mkDocString?` allows generating a dynamic docstring; if this is provided, `docString?` is ignored
+- `explicit` makes the hover pretty print the head application in explicit mode;
+  the default value is `false` (note: delaboration expression hovers normally set this to `true`,
+  since their purpose is to get more information about a given expression)
+-/
+def withExprHover (fmt : Format) (expr : Expr) (lctx : LocalContext)
+    (location? : Option DeclarationLocation := none)
+    (docString? : Option String := none)
+    (mkDocString? : Option (PPContext → IO String) := none)
+    (explicit : Bool := false) : MessageData :=
+  .ofFormatWithInfos {
+      fmt := .tag 0 fmt
+      infos :=
+        .ofList [(0, Elab.Info.ofDelabTermInfo {
+          expr, lctx, location?, explicit,
+          stx := .missing, -- unused for delaborator hovers
+          expectedType? := none, -- unused for delaborator hovers
+          elaborator := `Delab.withExprHover,
+          mkDocString? := mkDocString? <|> docString?.map (fun _ => pure ·)
+        })]
+  }
+
+/--
+Calls `withExprHover`, but uses the current local context if one is not given.
+See `withExprHover` for a description of each parameter.
+-/
+def withExprHoverM {m} [Monad m] [MonadLCtx m]
+    (fmt : Format) (expr : Expr) (lctx? : Option LocalContext := none)
+    (location? : Option DeclarationLocation := none)
+    (docString? : Option String := none)
+    (mkDocString? : Option (PPContext → IO String) := none)
+    (explicit : Bool := false) : m MessageData := do
+  let lctx ← lctx?.getDM getLCtx
+  return withExprHover fmt expr lctx location? docString? mkDocString? explicit
+
 partial def hasSyntheticSorry (msg : MessageData) : Bool :=
   visit none msg
 where