feat: refine declaration ranges at instance & example

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`.

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

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"}}