Provides an IpcM monad for interacting with an external LSP process. Used for testing the Lean server.
Instances For
def
Lean.Lsp.Ipc.writeNotification
{α : Type u_1}
[Lean.ToJson α]
(n : Lean.JsonRpc.Notification α)
:
Instances For
Instances For
def
Lean.Lsp.Ipc.readResponseAs
(expectedID : Lean.JsonRpc.RequestID)
(α : Type)
[Lean.FromJson α]
:
Instances For
def
Lean.Lsp.Ipc.collectDiagnostics
(waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0)
(target : Lean.Lsp.DocumentUri)
(version : Nat)
:
Waits for the worker to emit all diagnostics for the current document version and returns them as a list.
Instances For
partial def
Lean.Lsp.Ipc.collectDiagnostics.loop
(waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0)
:
def
Lean.Lsp.Ipc.runWith
{α : Type}
(lean : Lake.FilePath)
(args : optParam (Array String) #[])
(test : Lean.Lsp.Ipc.IpcM α)
:
IO α