From 59c33d24231fb9abf8362ee4aa42b55cda899049 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 25 Jan 2023 10:15:29 +0100
Subject: [PATCH] remove custom getDiagnostics

---
 server/leanserver/GameServer/RpcHandlers.lean | 29 -------------------
 1 file changed, 29 deletions(-)

diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
index 06b265f..c17eb40 100644
--- a/server/leanserver/GameServer/RpcHandlers.lean
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -126,33 +126,4 @@ builtin_initialize
     (Option GameInteractiveGoals)
     getInteractiveGoals
 
-structure Diagnostic where
-  severity : Option Lean.Lsp.DiagnosticSeverity
-  message : String
-deriving FromJson, ToJson
-
-open RequestM in
-def getDiagnostics (params : GetInteractiveDiagnosticsParams) : RequestM (RequestTask (Array Diagnostic)) := do
-  let doc ← readDoc
-  let rangeEnd := params.lineRange?.map fun range =>
-    doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
-  let t := doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
-  pure <| t.map fun (snaps, _) =>
-    let diags? := snaps.getLast?.map fun snap =>
-      snap.interactiveDiags.toArray.filterMap fun diag =>
-        if 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
-        then some {message := diag.message.stripTags, severity := diag.severity?}
-        else none
-    pure <| diags?.getD #[]
-
-builtin_initialize
-  registerBuiltinRpcProcedure
-    `Game.getDiagnostics
-    GetInteractiveDiagnosticsParams
-    (Array Diagnostic)
-    getDiagnostics
-
 end GameServer