Reading/writing LSP messages from/to IO handles.

def Lean.IO.FS.Stream.readLspMessage (h : IO.FS.Stream) : IO JsonRpc.Message

Equations

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

def Lean.IO.FS.Stream.readLspMessageAsString (h : IO.FS.Stream) : IO String

Equations

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

def Lean.IO.FS.Stream.readLspRequestAs (h : IO.FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO (JsonRpc.Request α)

Equations

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

def Lean.IO.FS.Stream.readLspNotificationAs (h : IO.FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO (JsonRpc.Notification α)

Equations

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

def Lean.IO.FS.Stream.readLspResponseAs (h : IO.FS.Stream) (expectedID : JsonRpc.RequestID) (α : Type) [FromJson α] : IO (JsonRpc.Response α)

Equations

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

def Lean.IO.FS.Stream.writeSerializedLspMessage (h : IO.FS.Stream) (msg : String) : IO Unit

Equations

• Lean.IO.FS.Stream.writeSerializedLspMessage h msg = do h.putStr (toString "Content-Length: " ++ toString (toString msg.utf8ByteSize) ++ toString "\x0d\n\x0d\n" ++ msg) h.flush

def Lean.IO.FS.Stream.writeLspMessage (h : IO.FS.Stream) (msg : JsonRpc.Message) : IO Unit

Equations

• Lean.IO.FS.Stream.writeLspMessage h msg = Lean.IO.FS.Stream.writeSerializedLspMessage h (Lean.toJson msg).compress

def Lean.IO.FS.Stream.writeLspRequest {α : Type u_1} [ToJson α] (h : IO.FS.Stream) (r : JsonRpc.Request α) : IO Unit

Equations

• Lean.IO.FS.Stream.writeLspRequest h r = Lean.IO.FS.Stream.writeLspMessage h (Lean.JsonRpc.Message.request r.id r.method (Lean.Json.toStructured? r.param).toOption)

def Lean.IO.FS.Stream.writeLspNotification {α : Type u_1} [ToJson α] (h : IO.FS.Stream) (n : JsonRpc.Notification α) : IO Unit

Equations

• Lean.IO.FS.Stream.writeLspNotification h n = Lean.IO.FS.Stream.writeLspMessage h (Lean.JsonRpc.Message.notification n.method (Lean.Json.toStructured? n.param).toOption)

def Lean.IO.FS.Stream.writeLspResponse {α : Type u_1} [ToJson α] (h : IO.FS.Stream) (r : JsonRpc.Response α) : IO Unit

Equations

• Lean.IO.FS.Stream.writeLspResponse h r = Lean.IO.FS.Stream.writeLspMessage h (Lean.JsonRpc.Message.response r.id (Lean.toJson r.result))

def Lean.IO.FS.Stream.writeLspResponseError (h : IO.FS.Stream) (e : JsonRpc.ResponseError Unit) : IO Unit

Equations

• Lean.IO.FS.Stream.writeLspResponseError h e = Lean.IO.FS.Stream.writeLspMessage h (Lean.JsonRpc.Message.responseError e.id e.code e.message none)

def Lean.IO.FS.Stream.writeLspResponseErrorWithData {α : Type u_1} [ToJson α] (h : IO.FS.Stream) (e : JsonRpc.ResponseError α) : IO Unit

Equations

• Lean.IO.FS.Stream.writeLspResponseErrorWithData h e = Lean.IO.FS.Stream.writeLspMessage h (Lean.JsonRpc.Message.responseError e.id e.code e.message (Option.map Lean.toJson e.data?))