Reading/writing LSP messages from/to IO handles.

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

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

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

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

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

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

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

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

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

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