Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) for use in the LSP server.

inductive Lean.JsonRpc.RequestID : Type

In JSON-RPC, each request from the client editor to the language server comes with a request id so that the corresponding response can be identified or cancelled.

• str (s : String) : RequestID
• num (n : JsonNumber) : RequestID
• null : RequestID

instance Lean.JsonRpc.instInhabitedRequestID : Inhabited RequestID

instance Lean.JsonRpc.instBEqRequestID : BEq RequestID

instance Lean.JsonRpc.instOrdRequestID : Ord RequestID

instance Lean.JsonRpc.instOfNatRequestID {n : Nat} : OfNat RequestID n

instance Lean.JsonRpc.instToStringRequestID : ToString RequestID

inductive Lean.JsonRpc.ErrorCode : Type

Error codes defined by JSON-RPC and LSP.

• parseError : ErrorCode

  Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.

• invalidRequest : ErrorCode

  The JSON sent is not a valid Request object.

• methodNotFound : ErrorCode

  The method does not exist / is not available.

• invalidParams : ErrorCode

  Invalid method parameter(s).

• internalError : ErrorCode

  Internal JSON-RPC error.

• serverNotInitialized : ErrorCode

  Error code indicating that a server received a notification or request before the server has received the initialize request.

• unknownErrorCode : ErrorCode
• contentModified : ErrorCode

  The server detected that the content of a document got modified outside normal conditions. A server should NOT send this error code if it detects a content change in it unprocessed messages. The result even computed on an older state might still be useful for the client.

  If a client decides that a result is not of any use anymore the client should cancel the request.

• requestCancelled : ErrorCode

  The client has canceled a request and a server as detected the cancel.

• rpcNeedsReconnect : ErrorCode
• workerExited : ErrorCode
• workerCrashed : ErrorCode

instance Lean.JsonRpc.instInhabitedErrorCode : Inhabited ErrorCode

instance Lean.JsonRpc.instBEqErrorCode : BEq ErrorCode

instance Lean.JsonRpc.instFromJsonErrorCode : FromJson ErrorCode

instance Lean.JsonRpc.instToJsonErrorCode : ToJson ErrorCode

inductive Lean.JsonRpc.Message : Type

A JSON-RPC message.

Uses separate constructors for notifications and errors because client and server behavior is expected to be wildly different for both.

• request (id : RequestID) (method : String) (params? : Option Json.Structured) : Message

  A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• notification (method : String) (params? : Option Json.Structured) : Message

  A notification message. A processed notification message must not send a response back. They work like events.

• response (id : RequestID) (result : Json) : Message

  A Response Message sent as a result of a request.

• responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) : Message

  A non-successful response.

instance Lean.JsonRpc.instInhabitedMessage : Inhabited Message

def Lean.JsonRpc.Batch : Type

structure Lean.JsonRpc.Request (α : Type u) : Type u

Generic version of Message.request.

A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• LSP
• JSON-RPC

• id : RequestID
• method : String
• param : α

instance Lean.JsonRpc.instInhabitedRequest {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Request a✝)

instance Lean.JsonRpc.instBEqRequest {α✝ : Type u_1} [BEq α✝] : BEq (Request α✝)

instance Lean.JsonRpc.instCoeOutRequestMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Request α) Message

structure Lean.JsonRpc.Notification (α : Type u) : Type u

Generic version of Message.notification.

A notification message. A processed notification message must not send a response back. They work like events.

• JSON-RPC
• LSP.

• method : String
• param : α

instance Lean.JsonRpc.instInhabitedNotification {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Notification a✝)

instance Lean.JsonRpc.instBEqNotification {α✝ : Type u_1} [BEq α✝] : BEq (Notification α✝)

instance Lean.JsonRpc.instCoeOutNotificationMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Notification α) Message

structure Lean.JsonRpc.Response (α : Type u) : Type u

Generic version of Message.response.

A Response Message sent as a result of a request. If a request doesn’t provide a result value the receiver of a request still needs to return a response message to conform to the JSON-RPC specification. The result property of the ResponseMessage should be set to null in this case to signal a successful request.

References:

• JSON-RPC
• LSP

• id : RequestID
• result : α

instance Lean.JsonRpc.instInhabitedResponse {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Response a✝)

instance Lean.JsonRpc.instBEqResponse {α✝ : Type u_1} [BEq α✝] : BEq (Response α✝)

instance Lean.JsonRpc.instCoeOutResponseMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Response α) Message

structure Lean.JsonRpc.ResponseError (α : Type u) : Type u

Generic version of Message.responseError.

References:

• JSON-RPC
• LSP.

• id : RequestID
• code : ErrorCode
• message : String

  A string providing a short description of the error.

• data? : Option α

  A primitive or structured value that contains additional information about the error. Can be omitted.

instance Lean.JsonRpc.instInhabitedResponseError {a✝ : Type u_1} : Inhabited (ResponseError a✝)

instance Lean.JsonRpc.instBEqResponseError {α✝ : Type u_1} [BEq α✝] : BEq (ResponseError α✝)

instance Lean.JsonRpc.instCoeOutResponseErrorMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (ResponseError α) Message

instance Lean.JsonRpc.instCoeOutResponseErrorUnitMessage : CoeOut (ResponseError Unit) Message

instance Lean.JsonRpc.instCoeStringRequestID : Coe String RequestID

instance Lean.JsonRpc.instCoeJsonNumberRequestID : Coe JsonNumber RequestID

instance Lean.JsonRpc.instLTRequestID : LT RequestID

instance Lean.JsonRpc.instDecidableLtRequestID (a b : RequestID) : Decidable (a < b)

instance Lean.JsonRpc.instFromJsonRequestID : FromJson RequestID

instance Lean.JsonRpc.instToJsonRequestID : ToJson RequestID

instance Lean.JsonRpc.instToJsonMessage : ToJson Message

instance Lean.JsonRpc.instFromJsonMessage : FromJson Message

instance Lean.JsonRpc.instFromJsonNotification {α : Type} [FromJson α] : FromJson (Notification α)

def IO.FS.Stream.readMessage (h : Stream) (nBytes : Nat) : IO Lean.JsonRpc.Message

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

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

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

def IO.FS.Stream.writeMessage (h : Stream) (m : Lean.JsonRpc.Message) : IO Unit

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

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

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

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

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