diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 36996dd428a7..4ff2087f5c70 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -229,6 +229,10 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
         | some v => m.insert p.fst $ f v p.snd)
 end Lean.HashMap
 
+/--
+Groups all elements `x`, `y` in `xs` with `key x == key y` into the same array
+`(xs.groupByKey key).find! (key x)`. Groups preserve the relative order of elements in `xs`.
+-/
 def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β)
     : Lean.HashMap α (Array β) := Id.run do
   let mut groups := ∅
diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean
index a15166b8d8cb..0112a6ead0a0 100644
--- a/src/Lean/Data/Lsp/Internal.lean
+++ b/src/Lean/Data/Lsp/Internal.lean
@@ -8,6 +8,8 @@ Authors: Joscha Mennicken
 import Lean.Expr
 import Lean.Data.Lsp.Basic
 
+set_option linter.missingDocs true -- keep it documented
+
 /-! This file contains types for communication between the watchdog and the
 workers. These messages are not visible externally to users of the LSP server.
 -/
@@ -17,17 +19,27 @@ namespace Lean.Lsp
 /-! Most reference-related types have custom FromJson/ToJson implementations to
 reduce the size of the resulting JSON. -/
 
+/--
+Identifier of a reference.
+-/
 inductive RefIdent where
+  /-- Named identifier. These are used in all references that are globally available. -/
   | const : Name → RefIdent
+  /-- Unnamed identifier. These are used for all local references. -/
   | fvar  : FVarId → RefIdent
   deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
+/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
 def toString : RefIdent → String
   | RefIdent.const n => s!"c:{n}"
   | RefIdent.fvar id => s!"f:{id.name}"
 
+/--
+Converts the string representation of a reference identifier back to a reference identifier.
+The string representation must have been created by `RefIdent.toString`.
+-/
 def fromString (s : String) : Except String RefIdent := do
   let sPrefix := s.take 2
   let sName := s.drop 2
@@ -53,18 +65,31 @@ instance : ToJson RefIdent where
 
 end RefIdent
 
+/-- Information about the declaration surrounding a reference. -/
 structure RefInfo.ParentDecl where
+  /-- Name of the declaration surrounding a reference. -/
   name           : Name
+  /-- Range of the declaration surrounding a reference. -/
   range          : Lsp.Range
+  /-- Selection range of the declaration surrounding a reference. -/
   selectionRange : Lsp.Range
   deriving ToJson
 
+/--
+Denotes the range of a reference, as well as the parent declaration of the reference.
+If the reference is itself a declaration, then it contains no parent declaration.
+-/
 structure RefInfo.Location where
+  /-- Range of the reference. -/
   range       : Lsp.Range
+  /-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
   parentDecl? : Option RefInfo.ParentDecl
 
+/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
 structure RefInfo where
+  /-- Definition site of the reference. May be `none` when we cannot find a definition site. -/
   definition? : Option RefInfo.Location
+  /-- Usage sites of the reference. -/
   usages      : Array RefInfo.Location
 
 instance : ToJson RefInfo where
@@ -135,6 +160,7 @@ Contains the file's definitions and references. -/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
   version    : Nat
+  /-- All references for the file. -/
   references : ModuleRefs
   deriving FromJson, ToJson
 
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index 9c8a97e227b5..49a4c87323d9 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -88,6 +88,11 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
 end FileMap
 end Lean
 
+/--
+Convert the Lean `DeclarationRange` to an LSP `Range` by turning the 1-indexed line numbering into a
+0-indexed line numbering and converting the character offset within the line to a UTF-16 indexed
+offset.
+-/
 def Lean.DeclarationRange.toLspRange (r : Lean.DeclarationRange) : Lsp.Range := {
   start := ⟨r.pos.line - 1, r.charUtf16⟩
   «end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 5d35051f2544..dbf487a321b8 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -175,7 +175,7 @@ all references of an identifier:
 - Chains of helper definitions like those created for do-reassignment `x := e`
 - Overlapping definitions like those defined by `where` declarations that define both an FVar
   (for local usage) and a constant (for non-local usage)
-- Identifiers connected by `FVarAliasInfo`
+- Identifiers connected by `FVarAliasInfo` such as variables before and after `match` generalization
 
 In the first three cases that are not explicitly denoted as aliases with an `FVarAliasInfo`, the
 corresponding `Reference`s have the exact same range.