feat: add range parameter to getInteractiveDiagnostics

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

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