From a329896e7036b37583071121c6e17a56837c2157 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 26 Nov 2021 17:11:14 +0100
Subject: [PATCH] feat: refine declaration ranges at `instance` & `example`

---
 src/Lean/Elab/DeclarationRange.lean            | 18 ++++++++++++++----
 tests/lean/interactive/hover.lean              |  5 +++++
 tests/lean/interactive/hover.lean.expected.out | 14 ++++++++++++++
 3 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/DeclarationRange.lean b/src/Lean/Elab/DeclarationRange.lean
index cebb5b1133..8d11137fd8 100644
--- a/src/Lean/Elab/DeclarationRange.lean
+++ b/src/Lean/Elab/DeclarationRange.lean
@@ -27,14 +27,24 @@ def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m Declaratio
   ```
   "def " >> declId >> optDeclSig >> declVal
   ```
-  For instances, we use the whole header since the name is optional.
+  If the declaration name is absent, we use the keyword instead.
   This function converts the given `Syntax` into one that represents its "selection range".
 -/
 def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
-  if stx.getKind == ``Parser.Command.«instance» then
-    stx.setArg 5 mkNullNode
+  if stx.isOfKind ``Lean.Parser.Command.instance then
+    -- must skip `attrKind` and `optPrio` for `instance`
+    if !stx[3].isNone then
+      stx[3][0]
+    else
+      stx[1]
   else
-    stx[1]
+    if stx[1][0].isIdent then
+      stx[1][0]  -- `declId`
+    else if stx[1].isIdent then
+      stx[1]  -- raw `ident`
+    else
+      stx[0]
+
 
 /--
   Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object decribing `declName`.
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index b0220ca442..580c7cc8ef 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -129,3 +129,8 @@ inductive Bar
         --^ textDocument/hover
   | mk : Bar
   --^ textDocument/hover
+
+instance : ToString Nat := ⟨toString⟩
+--^ textDocument/hover
+instance f : ToString Nat := ⟨toString⟩
+       --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 35349cf05a..5df3cf0caf 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -145,3 +145,17 @@ null
  {"start": {"line": 129, "character": 4}, "end": {"line": 129, "character": 6}},
  "contents":
  {"value": "```lean\nBar.Bar.mk : Bar.Bar\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 132, "character": 2}}
+{"range":
+ {"start": {"line": 132, "character": 0}, "end": {"line": 132, "character": 8}},
+ "contents":
+ {"value": "```lean\nBar.instToStringNat : ToString Nat\n```",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 134, "character": 9}}
+{"range":
+ {"start": {"line": 134, "character": 9},
+  "end": {"line": 134, "character": 10}},
+ "contents":
+ {"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}}