diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 1b1adff4d5..953bde99d1 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -147,13 +147,11 @@ partial def combineFvars (refs : Array Reference) : Array Reference := Id.run do let mut refs' := #[] for ref in refs do match ref with - | { ident := RefIdent.fvar id, range, isBinder := true } => - -- Since deduplication works via definitions, we know that a definition - -- for the base id exists. - unless idMap.contains id do -- Only keep the base definition - refs' := refs'.push ref - | { ident, range, isBinder := false } => - refs' := refs'.push { ident := applyIdMap idMap ident, range, isBinder := false } + | { ident := ident@(RefIdent.fvar id), range, isBinder } => + -- downgrade chained definitions to usages + -- (we shouldn't completely remove them in case they do not have usages) + let isBinder := isBinder && !idMap.contains id + refs' := refs'.push { ident := applyIdMap idMap ident, range, isBinder } | _ => refs' := refs'.push ref refs' diff --git a/tests/lean/interactive/highlight.lean b/tests/lean/interactive/highlight.lean index df00ee3100..59bc9e2d6a 100644 --- a/tests/lean/interactive/highlight.lean +++ b/tests/lean/interactive/highlight.lean @@ -41,3 +41,10 @@ example : Nat := Id.run do return y pure y --^ textDocument/documentHighlight + +example : Nat := Id.run do + let mut y := 0 + if true then + y := 1 + return y -- TODO: definition should be first `y` + --^ textDocument/documentHighlight diff --git a/tests/lean/interactive/highlight.lean.expected.out b/tests/lean/interactive/highlight.lean.expected.out index 777450ed75..fff839d035 100644 --- a/tests/lean/interactive/highlight.lean.expected.out +++ b/tests/lean/interactive/highlight.lean.expected.out @@ -104,3 +104,15 @@ {"range": {"start": {"line": 41, "character": 7}, "end": {"line": 41, "character": 8}}, "kind": 1}] +{"textDocument": {"uri": "file://highlight.lean"}, + "position": {"line": 48, "character": 9}} +[{"range": + {"start": {"line": 47, "character": 4}, "end": {"line": 47, "character": 5}}, + "kind": 1}, + {"range": + {"start": {"line": 45, "character": 10}, + "end": {"line": 45, "character": 11}}, + "kind": 1}, + {"range": + {"start": {"line": 48, "character": 9}, "end": {"line": 48, "character": 10}}, + "kind": 1}]