class Lapis.Transport.Transport (T : Type) : Type

• readMessage : T → IO (Option Protocol.JsonRpc.Message)
• writeMessage : T → Protocol.JsonRpc.Message → IO Unit
• close : T → IO Unit

Writer Actor for Output Channel

structure Lapis.Transport.OutputChannel : Type

A thread-safe output channel for sending messages to the client

• state : Lapis.Transport.WriterState✝

  Writer state

• task : Task (Except IO.Error Unit)

  Writer task

def Lapis.Transport.OutputChannel.new (writeFunc : Protocol.JsonRpc.Message → IO Unit) : IO OutputChannel

Create a new output channel with a writer actor

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Transport.OutputChannel.send (ch : OutputChannel) (msg : Protocol.JsonRpc.Message) : IO Unit

Send a message through the output channel (non-blocking)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Transport.OutputChannel.sendNotification (ch : OutputChannel) (method : String) (params : Lean.Json) : IO Unit

Send a notification through the output channel

Equations

• ch.sendNotification method params = ch.send (Lapis.Protocol.JsonRpc.Message.notification { method := method, params := some params })

def Lapis.Transport.OutputChannel.sendRequest (ch : OutputChannel) (id : Protocol.JsonRpc.RequestId) (method : String) (params : Lean.Json) : IO Unit

Send a request through the output channel

Equations

• ch.sendRequest id method params = ch.send (Lapis.Protocol.JsonRpc.Message.request { id := id, method := method, params := some params })

def Lapis.Transport.OutputChannel.shutdown (ch : OutputChannel) : IO Unit

Shutdown the writer actor

Equations

• One or more equations did not get rendered due to their size.