From 9b842b7554b932f51bd7efe4e76791dd596025ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 20 Sep 2025 01:02:12 -0700
Subject: [PATCH] fix: message context in `grind` code actions (#10473)

This PR ensures the code action messages produced by `grind` include the
full context
---
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 840897d9f4..88061c365c 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -1396,7 +1396,9 @@ def EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax ``Par
 private def save (ref : Syntax) (thm : EMatchTheorem) (isParam : Bool) (minIndexable : Bool) : SelectM Unit := do
   -- We only save `thm` if the pattern is different from the ones that were already found.
   if (← get).thms.all fun thm' => thm.patterns != thm'.patterns then
-    let pats ← thm.patterns.mapM fun p => (ppPattern p).toString
+    let pats ← thm.patterns.mapM fun p => do
+      let pats ← addMessageContextFull (ppPattern p)
+      pats.format
     let openBracket  := if isParam then "" else "["
     let closeBracket := if isParam then "" else "]"
     let msg := s!"{closeBracket} for pattern: {pats}"