Documentation

Lean.Data.Lsp.Ipc

def Lean.Lsp.Ipc.ipcStdioConfig :

IO.Process.StdioConfig

Equations

Lean.Lsp.Ipc.ipcStdioConfig = { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.inherit }

@[inline]

abbrev Lean.Lsp.Ipc.IpcM (α : Type) :

Type

Equations

Lean.Lsp.Ipc.IpcM = ReaderT (IO.Process.Child Lean.Lsp.Ipc.ipcStdioConfig) IO

def Lean.Lsp.Ipc.stdin :

Lean.Lsp.Ipc.IpcM IO.FS.Stream

Equations

Lean.Lsp.Ipc.stdin = do let a ← read pure (IO.FS.Stream.ofHandle a.stdin)

def Lean.Lsp.Ipc.stdout :

Lean.Lsp.Ipc.IpcM IO.FS.Stream

Equations

Lean.Lsp.Ipc.stdout = do let a ← read pure (IO.FS.Stream.ofHandle a.stdout)

def Lean.Lsp.Ipc.writeRequest {α : Type u_1} [inst : Lean.ToJson α] (r : Lean.JsonRpc.Request α) :

Lean.Lsp.Ipc.IpcM Unit

Equations

Lean.Lsp.Ipc.writeRequest r = do let a ← Lean.Lsp.Ipc.stdin liftM (IO.FS.Stream.writeLspRequest a r)

def Lean.Lsp.Ipc.writeNotification {α : Type u_1} [inst : Lean.ToJson α] (n : Lean.JsonRpc.Notification α) :

Lean.Lsp.Ipc.IpcM Unit

Equations

Lean.Lsp.Ipc.writeNotification n = do let a ← Lean.Lsp.Ipc.stdin liftM (IO.FS.Stream.writeLspNotification a n)

def Lean.Lsp.Ipc.readMessage :

Lean.Lsp.Ipc.IpcM Lean.JsonRpc.Message

Equations

Lean.Lsp.Ipc.readMessage = do let a ← Lean.Lsp.Ipc.stdout liftM (IO.FS.Stream.readLspMessage a)

def Lean.Lsp.Ipc.readRequestAs (expectedMethod : String) (α : Type) [inst : Lean.FromJson α] :

Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Request α)

Equations

Lean.Lsp.Ipc.readRequestAs expectedMethod α = do let a ← Lean.Lsp.Ipc.stdout liftM (IO.FS.Stream.readLspRequestAs a expectedMethod α)

def Lean.Lsp.Ipc.readResponseAs (expectedID : Lean.JsonRpc.RequestID) (α : Type) [inst : Lean.FromJson α] :

Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Response α)

Equations

Lean.Lsp.Ipc.readResponseAs expectedID α = do let a ← Lean.Lsp.Ipc.stdout liftM (IO.FS.Stream.readLspResponseAs a expectedID α)

def Lean.Lsp.Ipc.waitForExit :

Lean.Lsp.Ipc.IpcM UInt32

Equations

Lean.Lsp.Ipc.waitForExit = do let a ← read liftM (IO.Process.Child.wait a)

def Lean.Lsp.Ipc.collectDiagnostics (waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0) (target : Lean.Lsp.DocumentUri) (version : Nat) :

Lean.Lsp.Ipc.IpcM (List (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))

Equations

Lean.Lsp.Ipc.collectDiagnostics waitForDiagnosticsId target version = do Lean.Lsp.Ipc.writeRequest { id := waitForDiagnosticsId, method := "textDocument/waitForDiagnostics", param := { uri := target, version := version } } (fun loop => loop) (Lean.Lsp.Ipc.collectDiagnostics.loop waitForDiagnosticsId)

partial def Lean.Lsp.Ipc.collectDiagnostics.loop (waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0) :

Lean.Lsp.Ipc.IpcM (List (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))

def Lean.Lsp.Ipc.runWith {α : Type} (lean : System.FilePath) (args : optParam (Array String) #[]) (test : Lean.Lsp.Ipc.IpcM α) :

IO α

Equations

Lean.Lsp.Ipc.runWith lean args test = do let proc ← IO.Process.spawn { toStdioConfig := Lean.Lsp.Ipc.ipcStdioConfig, cmd := lean.toString, args := args, cwd := none, env := #[] } ReaderT.run test proc