Documentation

Lean.Data.Lsp.Communication

Reading/writing LSP messages from/to IO handles.

def IO.FS.Stream.readLspMessage (h : IO.FS.Stream) :

IO Lean.JsonRpc.Message

Equations

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

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

IO (Lean.JsonRpc.Request α)

Equations

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

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

IO (Lean.JsonRpc.Notification α)

Equations

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

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

IO (Lean.JsonRpc.Response α)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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