Equations
- IO.FS.Stream.readLspMessage h = tryCatch (do let nBytes ← IO.FS.Stream.readLspHeader h IO.FS.Stream.readMessage h nBytes) fun e => throw (IO.userError (toString "Cannot read LSP message: " ++ toString e ++ toString ""))
def
IO.FS.Stream.readLspRequestAs
(h : IO.FS.Stream)
(expectedMethod : String)
(α : Type)
[inst : Lean.FromJson α]
:
Equations
- IO.FS.Stream.readLspRequestAs h expectedMethod α = tryCatch (do let nBytes ← IO.FS.Stream.readLspHeader h IO.FS.Stream.readRequestAs h nBytes expectedMethod α) fun e => throw (IO.userError (toString "Cannot read LSP request: " ++ toString e ++ toString ""))
def
IO.FS.Stream.readLspNotificationAs
(h : IO.FS.Stream)
(expectedMethod : String)
(α : Type)
[inst : Lean.FromJson α]
:
Equations
- IO.FS.Stream.readLspNotificationAs h expectedMethod α = tryCatch (do let nBytes ← IO.FS.Stream.readLspHeader h IO.FS.Stream.readNotificationAs h nBytes expectedMethod α) fun e => throw (IO.userError (toString "Cannot read LSP notification: " ++ toString e ++ toString ""))
def
IO.FS.Stream.readLspResponseAs
(h : IO.FS.Stream)
(expectedID : Lean.JsonRpc.RequestID)
(α : Type)
[inst : Lean.FromJson α]
:
Equations
- IO.FS.Stream.readLspResponseAs h expectedID α = tryCatch (do let nBytes ← IO.FS.Stream.readLspHeader h IO.FS.Stream.readResponseAs h nBytes expectedID α) fun e => throw (IO.userError (toString "Cannot read LSP response: " ++ toString e ++ toString ""))
Equations
- IO.FS.Stream.writeLspMessage h msg = let j := Lean.Json.compress (Lean.toJson msg); let header := toString "Content-Length: " ++ toString (toString (String.utf8ByteSize j)) ++ toString "\x0d\n\x0d\n"; do IO.FS.Stream.putStr h (header ++ j) h.flush
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))
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?))