fix: reference fields in constructor correctly

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)

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 :=

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