diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 5ba7d03cc7..2b76ca4f50 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -155,37 +155,40 @@ partial def handleReferences (p : ReferenceParams) mapTask t fun (snaps, _) => do if let some snap := snaps.find? (fun s => s.endPos > hoverPos) then if let some (ci, i) := snap.infoTree.hoverableInfoAt? hoverPos then - if let Info.ofTermInfo ti := i then - if let some ident := identOf ti.expr then - let refs := List.join <| snaps.map (findReferences doc) - return referencesTo doc ident (p.context.includeDeclaration) refs + if let some (ident, isDecl) := identOf i then + let refs := List.join <| snaps.map (findReferences doc) + return referencesTo doc ident (p.context.includeDeclaration) refs return #[] where - identOf : Expr → Option RefIdent - | Expr.const n .. => some (RefIdent.name n) - | Expr.fvar id .. => some (RefIdent.fvar id) + identOf : Info → Option (RefIdent × Bool) + | Info.ofTermInfo ti => match ti.expr with + | Expr.const n .. => some (RefIdent.name n, ti.isBinder) + | Expr.fvar id .. => some (RefIdent.fvar id, ti.isBinder) + | _ => none + | Info.ofFieldInfo fi => some (RefIdent.name fi.projName, false) | _ => none - addReference (doc : EditableDocument) (ident : RefIdent) (ti : TermInfo) (refs : List Reference) - : List Reference := - if let some range := ti.stx.getRange? (originalOnly := true) then + addReference (doc : EditableDocument) (info : Info) + (ident : RefIdent) (isDeclaration : Bool) + (refs : List Reference) : List Reference := + if let some range := info.stx.getRange? (originalOnly := true) then let text := doc.meta.text let range := { start := text.utf8PosToLspPos range.start «end» := text.utf8PosToLspPos range.stop } - { ident, range, isDeclaration := ti.isBinder } :: refs + { ident, range, isDeclaration } :: refs else refs findReferences (doc : EditableDocument) (snap : Snapshot) : List Reference := let infos := snap.infoTree.findAll fun | Info.ofTermInfo _ => true + | Info.ofFieldInfo _ => true | _ => false infos.foldl (init := []) fun refs info => do - if let Info.ofTermInfo ti := info then - if let some ident := identOf ti.expr then - return addReference doc ident ti refs + if let some (ident, isDecl) := identOf info then + return addReference doc info ident isDecl refs return refs referencesTo (doc : EditableDocument) (ident : RefIdent) (includeDecl : Bool) (refs : List Reference) diff --git a/tests/lean/interactive/references.lean b/tests/lean/interactive/references.lean index 1fe775ba65..19b75acd8f 100644 --- a/tests/lean/interactive/references.lean +++ b/tests/lean/interactive/references.lean @@ -17,7 +17,11 @@ structure Foo where def mkFoo : Foo := { a := 2 +--^ textDocument/references : {"context": {"includeDeclaration": true}} +--^ textDocument/references : {"context": {"includeDeclaration": false}} b := ⟨⟩ +--^ textDocument/references : {"context": {"includeDeclaration": true}} +--^ textDocument/references : {"context": {"includeDeclaration": false}} : Foo } def foo (x : Foo) : Nat := diff --git a/tests/lean/interactive/references.lean.expected.out b/tests/lean/interactive/references.lean.expected.out index 7f2c5489a9..5f468e1933 100644 --- a/tests/lean/interactive/references.lean.expected.out +++ b/tests/lean/interactive/references.lean.expected.out @@ -21,29 +21,29 @@ {"start": {"line": 4, "character": 10}, "end": {"line": 4, "character": 13}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 20, "character": 2}, "end": {"line": 20, "character": 5}}}, + {"start": {"line": 24, "character": 2}, "end": {"line": 24, "character": 5}}}, {"uri": "file://references.lean", "range": {"start": {"line": 17, "character": 12}, "end": {"line": 17, "character": 15}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 22, "character": 13}, - "end": {"line": 22, "character": 16}}}] + {"start": {"line": 26, "character": 13}, + "end": {"line": 26, "character": 16}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 4, "character": 10}, "context": {"includeDeclaration": false}} [{"uri": "file://references.lean", "range": - {"start": {"line": 20, "character": 2}, "end": {"line": 20, "character": 5}}}, + {"start": {"line": 24, "character": 2}, "end": {"line": 24, "character": 5}}}, {"uri": "file://references.lean", "range": {"start": {"line": 17, "character": 12}, "end": {"line": 17, "character": 15}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 22, "character": 13}, - "end": {"line": 22, "character": 16}}}] + {"start": {"line": 26, "character": 13}, + "end": {"line": 26, "character": 16}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 7, "character": 2}, "context": {"includeDeclaration": true}} @@ -52,15 +52,21 @@ {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 3}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 27, "character": 13}, - "end": {"line": 27, "character": 14}}}] + {"start": {"line": 18, "character": 2}, "end": {"line": 18, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 31, "character": 13}, + "end": {"line": 31, "character": 14}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 7, "character": 2}, "context": {"includeDeclaration": false}} [{"uri": "file://references.lean", "range": - {"start": {"line": 27, "character": 13}, - "end": {"line": 27, "character": 14}}}] + {"start": {"line": 18, "character": 2}, "end": {"line": 18, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 31, "character": 13}, + "end": {"line": 31, "character": 14}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 7, "character": 6}, "context": {"includeDeclaration": true}} @@ -69,18 +75,23 @@ {"start": {"line": 7, "character": 6}, "end": {"line": 7, "character": 9}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 22, "character": 20}, - "end": {"line": 22, "character": 23}}}] + {"start": {"line": 26, "character": 20}, + "end": {"line": 26, "character": 23}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 11, "character": 2}, "context": {"includeDeclaration": true}} [{"uri": "file://references.lean", "range": - {"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 3}}}] + {"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 3}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 11, "character": 2}, "context": {"includeDeclaration": false}} -[] +[{"uri": "file://references.lean", + "range": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 3}}}] {"textDocument": {"uri": "file://references.lean"}, "position": {"line": 11, "character": 6}, "context": {"includeDeclaration": true}} @@ -97,78 +108,105 @@ "range": {"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 9}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 22, "character": 4}, + "position": {"line": 18, "character": 2}, "context": {"includeDeclaration": true}} [{"uri": "file://references.lean", "range": - {"start": {"line": 22, "character": 4}, "end": {"line": 22, "character": 7}}}] + {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 18, "character": 2}, "end": {"line": 18, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 31, "character": 13}, + "end": {"line": 31, "character": 14}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 22, "character": 4}, + "position": {"line": 18, "character": 2}, + "context": {"includeDeclaration": false}} +[{"uri": "file://references.lean", + "range": + {"start": {"line": 18, "character": 2}, "end": {"line": 18, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 31, "character": 13}, + "end": {"line": 31, "character": 14}}}] +{"textDocument": {"uri": "file://references.lean"}, + "position": {"line": 21, "character": 2}, + "context": {"includeDeclaration": true}} +[{"uri": "file://references.lean", + "range": + {"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 3}}}, + {"uri": "file://references.lean", + "range": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 3}}}] +{"textDocument": {"uri": "file://references.lean"}, + "position": {"line": 21, "character": 2}, + "context": {"includeDeclaration": false}} +[{"uri": "file://references.lean", + "range": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 3}}}] +{"textDocument": {"uri": "file://references.lean"}, + "position": {"line": 26, "character": 4}, + "context": {"includeDeclaration": true}} +[{"uri": "file://references.lean", + "range": + {"start": {"line": 26, "character": 4}, "end": {"line": 26, "character": 7}}}] +{"textDocument": {"uri": "file://references.lean"}, + "position": {"line": 26, "character": 4}, "context": {"includeDeclaration": false}} [] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 22, "character": 9}, + "position": {"line": 26, "character": 9}, "context": {"includeDeclaration": true}} [{"uri": "file://references.lean", "range": - {"start": {"line": 22, "character": 9}, - "end": {"line": 22, "character": 10}}}, - {"uri": "file://references.lean", - "range": - {"start": {"line": 27, "character": 11}, - "end": {"line": 27, "character": 12}}}] + {"start": {"line": 26, "character": 9}, + "end": {"line": 26, "character": 10}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 22, "character": 9}, + "position": {"line": 26, "character": 9}, "context": {"includeDeclaration": false}} -[{"uri": "file://references.lean", - "range": - {"start": {"line": 27, "character": 11}, - "end": {"line": 27, "character": 12}}}] +[] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 27, "character": 11}, + "position": {"line": 31, "character": 11}, "context": {"includeDeclaration": true}} [{"uri": "file://references.lean", "range": - {"start": {"line": 22, "character": 9}, - "end": {"line": 22, "character": 10}}}, - {"uri": "file://references.lean", - "range": - {"start": {"line": 27, "character": 11}, - "end": {"line": 27, "character": 12}}}] + {"start": {"line": 31, "character": 11}, + "end": {"line": 31, "character": 12}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 27, "character": 11}, + "position": {"line": 31, "character": 11}, "context": {"includeDeclaration": false}} [{"uri": "file://references.lean", "range": - {"start": {"line": 27, "character": 11}, - "end": {"line": 27, "character": 12}}}] + {"start": {"line": 31, "character": 11}, + "end": {"line": 31, "character": 12}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 27, "character": 6}, + "position": {"line": 31, "character": 6}, "context": {"includeDeclaration": true}} [{"uri": "file://references.lean", "range": - {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 3}}}, + {"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 3}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 27, "character": 6}, "end": {"line": 27, "character": 7}}}] + {"start": {"line": 31, "character": 6}, "end": {"line": 31, "character": 7}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 27, "character": 6}, + "position": {"line": 31, "character": 6}, "context": {"includeDeclaration": false}} [{"uri": "file://references.lean", "range": - {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 3}}}] + {"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 3}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 32, "character": 2}, + "position": {"line": 36, "character": 2}, "context": {"includeDeclaration": true}} [{"uri": "file://references.lean", "range": - {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 3}}}, + {"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 3}}}, {"uri": "file://references.lean", "range": - {"start": {"line": 27, "character": 6}, "end": {"line": 27, "character": 7}}}] + {"start": {"line": 31, "character": 6}, "end": {"line": 31, "character": 7}}}] {"textDocument": {"uri": "file://references.lean"}, - "position": {"line": 32, "character": 2}, + "position": {"line": 36, "character": 2}, "context": {"includeDeclaration": false}} [{"uri": "file://references.lean", "range": - {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 3}}}] + {"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 3}}}]