From d2dcff1f9a20f95086bfe302a5da9b97d31c532d Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 31 Jan 2022 20:04:24 +0100
Subject: [PATCH] refactor: address review comments

---
 src/Lean/Server/FileWorker.lean | 4 ++++
 src/Lean/Server/References.lean | 2 +-
 src/Lean/Server/Watchdog.lean   | 6 +++---
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 92626ec381..688bf39b23 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -99,6 +99,8 @@ section Elab
     if lastSnap.isAtEnd then
       publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
       publishProgressDone m ctx.hOut
+      -- This will overwrite existing ilean info for the file, in case something
+      -- went wrong during the incremental updates.
       publishIleanInfoFinal m ctx.hOut <| s.snaps.insertAt 0 s.headerSnap
       return none
     publishProgressAtPos m lastSnap.endPos ctx.hOut
@@ -134,6 +136,8 @@ section Elab
       publishIleanInfoFinal m ctx.hOut #[headerSnap]
       AsyncList.nil
     else
+      -- This will overwrite existing ilean info for the file since this has a
+      -- higher version number.
       publishIleanInfoUpdate m ctx.hOut <| snaps.insertAt 0 headerSnap
       AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk) { headerSnap, snaps }
 end Elab
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 3597f5f068..42a4f20ca9 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -227,7 +227,7 @@ def referringTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPa
           result := result.push ⟨uri, range⟩
   result
 
-def definitionOf (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
+def definitionOf? (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
     : IO (Option Location) := do
   for (module, refs) in self.allRefs.toList do
     if let some info := refs.find? ident then
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 148ced0554..9e06fb0fd0 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -368,13 +368,13 @@ end ServerM
 
 section RequestHandling
 
-def findDefinition (p : TextDocumentPositionParams) : ServerM <| Option Location := do
+def findDefinition? (p : TextDocumentPositionParams) : ServerM <| Option Location := do
   if let some path := p.textDocument.uri.toPath? then
     let srcSearchPath := (← read).srcSearchPath
     if let some module ← searchModuleNameOfFileName path srcSearchPath then
       let references ← (← read).references.get
       if let some ident := references.findAt? module p.position then
-        return ← references.definitionOf ident srcSearchPath
+        return ← references.definitionOf? ident srcSearchPath
   return none
 
 def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
@@ -543,7 +543,7 @@ section MessageHandling
     -- go-to-type-definition.
     if method == "textDocument/definition" || method == "textDocument/declaration" then
       let params ← parseParams TextDocumentPositionParams params
-      if let some definition ← findDefinition params then
+      if let some definition ← findDefinition? params then
         (← read).hOut.writeLspResponse ⟨id, #[definition]⟩
         return
     match method with