From d6ba8e597a3d2fc2b33e2cfa3bc7c39485adef97 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 11 Oct 2021 18:59:03 +0200
Subject: [PATCH] feat: add range parameter to getInteractiveDiagnostics

---
 src/Lean/Data/Lsp/Extra.lean                   |  8 ++++++++
 src/Lean/Server/FileWorker/WidgetRequests.lean | 18 ++++++++++++++----
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean
index f00d9ee626..045536e3c6 100644
--- a/src/Lean/Data/Lsp/Extra.lean
+++ b/src/Lean/Data/Lsp/Extra.lean
@@ -137,4 +137,12 @@ structure RpcKeepAliveParams where
   sessionId : UInt64
   deriving FromJson, ToJson
 
+/--
+Range of lines in a document, including `start` but excluding `end`.
+-/
+structure LineRange where
+  start : Nat
+  «end» : Nat
+  deriving Inhabited, Repr, FromJson, ToJson
+
 end Lean.Lsp
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 1c0d3a385a..0c3afd28e4 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -67,16 +67,26 @@ builtin_initialize
     (Option InteractiveTermGoal)
     FileWorker.getInteractiveTermGoal
 
+structure GetInteractiveDiagnosticsParams where
+  lineRange? : Option Lsp.LineRange
+  deriving Inhabited, FromJson, ToJson
+
 open RequestM in
-def getInteractiveDiagnostics (_ : Json) : RequestM (RequestTask (Array InteractiveDiagnostic)) := do
+def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : RequestM (RequestTask (Array InteractiveDiagnostic)) := do
   let doc ← readDoc
-  let t₁ ← doc.cmdSnaps.waitAll
-  t₁.map fun (snaps, _) => snaps.getLast!.interactiveDiags.toArray
+  let rangeEnd ← params.lineRange?.map fun range =>
+    doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
+  withWaitFindSnap doc (fun snap => rangeEnd.all (· ≤ snap.endPos)) #[]
+    fun snap => snap.interactiveDiags.toArray.filter fun diag =>
+      params.lineRange?.all fun ⟨s, e⟩ =>
+        -- does [s,e) intersect [diag.fullRange.start.line,diag.fullRange.end.line)?
+        s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨
+        diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line
 
 builtin_initialize
   registerRpcCallHandler
     `Lean.Widget.getInteractiveDiagnostics
-    Json
+    GetInteractiveDiagnosticsParams
     (Array InteractiveDiagnostic)
     getInteractiveDiagnostics