diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 2fbca1d4f9..a4931bd969 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -213,13 +213,13 @@ section RequestHandling (this way, the server doesn't get bogged down in requests for an old state of the document). Requests need to manually check for whether their task has been cancelled, so that they can reply with a RequestCancelled error. -/ - def handleHover (id : RequestID) (p : HoverParams) : ServerM Unit := pure ⟨⟩ + def handleHover (id : RequestID) (p : HoverParams) : ServerM (Option Hover) := pure none - def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam) : ServerM Unit := do + def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam) : ServerM WaitForDiagnostics := do let st ← read let e ← st.docRef.get discard $ e.cmdSnaps.waitAll - st.hOut.writeLspResponse ⟨id, WaitForDiagnostics.mk⟩ + WaitForDiagnostics.mk end RequestHandling section MessageHandling @@ -236,19 +236,22 @@ section MessageHandling | "$/cancelRequest" => handle CancelParams handleCancelRequest | _ => throwServerError s!"Got unsupported notification method: {method}" - def queueRequest (id : RequestID) (handler : RequestID → α → ServerM Unit) (params : α) + def queueRequest (id : RequestID) (handleAct : ServerM Unit) : ServerM Unit := do - let requestTask ← asTask (handler id params (←read)) + let requestTask ← asTask (handleAct (←read)) updatePendingRequests (fun pendingRequests => pendingRequests.insert id requestTask) def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do - let handle := fun paramType [FromJson paramType] - (handler : RequestID → paramType → ServerM Unit) => - parseParams paramType params >>= queueRequest id handler + let handle := fun paramType [FromJson paramType] respType [ToJson respType] + (handler : RequestID → paramType → ServerM respType) => + queueRequest id do + let p ← parseParams paramType params + let resp ← handler id p + (←read).hOut.writeLspResponse ⟨id, resp⟩ match method with - | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam handleWaitForDiagnostics - | "textDocument/hover" => handle HoverParams handleHover + | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam WaitForDiagnostics handleWaitForDiagnostics + | "textDocument/hover" => handle HoverParams (Option Hover) handleHover | _ => throwServerError s!"Got unsupported request: {method}" end MessageHandling @@ -295,18 +298,6 @@ def initAndRunWorker (i o e : FS.Stream) : IO Unit := do } ReaderT.run (do handleDidOpen param; mainLoop) ctx -namespace Test - -def runWorkerWithInputFile (fn : String) (searchPath : Option String) : IO Unit := do - let o ← IO.getStdout - let e ← IO.getStderr - FS.withFile fn FS.Mode.read $ fun hFile => do - Lean.initSearchPath searchPath - try initAndRunWorker (FS.Stream.ofHandle hFile) o e - catch err => e.putStrLn (toString err) - -end Test - @[export lean_server_worker_main] def workerMain : IO UInt32 := do let i ← IO.getStdin diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 1ad7d89267..f21257051b 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -461,59 +461,6 @@ def initAndRunWatchdog (i o e : FS.Stream) : IO Unit := do : ServerContext } -namespace Test - -def watchdogCfg : Process.StdioConfig where - stdin := Process.Stdio.piped - stdout := Process.Stdio.piped - stderr := Process.Stdio.piped - -abbrev WatchdogM := ReaderT (Process.Child watchdogCfg) IO - -variable [ToJson α] - -def stdin : WatchdogM FS.Stream := do - FS.Stream.ofHandle (←read).stdin - -def stdout : WatchdogM FS.Stream := do - FS.Stream.ofHandle (←read).stdout - -def writeRequest (r : Request α) : WatchdogM Unit := do - (←stdin).writeLspRequest r - -def writeNotification (n : Notification α) : WatchdogM Unit := do - (←stdin).writeLspNotification n - -def readResponseAs (expectedID : RequestID) (α) [FromJson α] : WatchdogM (Response α) := do - (←stdout).readLspResponseAs expectedID α - -partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) -: WatchdogM (List (Notification PublishDiagnosticsParams)) := do - writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParam.mk target⟩ - let rec loop : WatchdogM (List (Notification PublishDiagnosticsParams)) := do - let error : IO (List (Notification PublishDiagnosticsParams)) := throw $ userError "Got unexpected packet while collecting diagnostics" - match ←(←stdout).readLspMessage with - | Message.response id _ => - if id = waitForDiagnosticsId then - [] - else - error - | Message.notification "textDocument/publishDiagnostics" (some param) => - match fromJson? (toJson param) with - | some diagnosticParam => ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop) - | none => error - | _ => error - loop - -def runWatchdogTest (test : WatchdogM Unit) : IO Unit := do - let proc ← Process.spawn { - toStdioConfig := watchdogCfg - cmd := ←IO.appPath - args := #["--server"] - } - ReaderT.run test proc -end Test - @[export lean_server_watchdog_main] def watchdogMain : IO UInt32 := do let i ← IO.getStdin