From c042e7ba58289f896da3a7a875a2cf62e51bca76 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Jul 2022 12:20:33 -0700
Subject: [PATCH] feat: add support for "jump-to-definition" at `[tactic ...]`,
 `[commandElab ...]` and `[termElab ...]` attributes

see #1350
---
 src/Lean/Elab/Util.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 96fa3b626b..71161d38ed 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -105,7 +105,18 @@ unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (
     name          := attrName
     descr         := kind ++ " elaborator"
     valueTypeName := typeName
-    evalKey       := fun _ stx => syntaxNodeKindOfAttrParam parserNamespace stx
+    evalKey       := fun _ stx => do
+      let kind ← syntaxNodeKindOfAttrParam parserNamespace stx
+      /- Recall that a `SyntaxNodeKind` is often the name of the paser, but this is not always true, and we much check it. -/
+      if (← getEnv).contains kind && (← getInfoState).enabled then
+        pushInfoLeaf <| Info.ofTermInfo {
+          elaborator    := .anonymous
+          lctx          := {}
+          expr          := mkConst kind
+          stx           := stx[1]
+          expectedType? := none
+        }
+      return kind
     onAdded       := fun builtin declName => do
       if builtin then
       if let some doc ← findDocString? (← getEnv) declName then