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

inductive Lean.JsonRpc.RequestID : Type

• str: String → Lean.JsonRpc.RequestID
• num: Lean.JsonNumber → Lean.JsonRpc.RequestID
• null: Lean.JsonRpc.RequestID

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.

instance Lean.JsonRpc.instInhabitedRequestID : Inhabited Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instBEqRequestID : BEq Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instOrdRequestID : Ord Lean.JsonRpc.RequestID

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

instance Lean.JsonRpc.instToStringRequestID : ToString Lean.JsonRpc.RequestID

inductive Lean.JsonRpc.ErrorCode : Type

• parseError: Lean.JsonRpc.ErrorCode

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

• invalidRequest: Lean.JsonRpc.ErrorCode

  The JSON sent is not a valid Request object.

• methodNotFound: Lean.JsonRpc.ErrorCode

  The method does not exist / is not available.

• invalidParams: Lean.JsonRpc.ErrorCode

  Invalid method parameter(s).

• internalError: Lean.JsonRpc.ErrorCode

  Internal JSON-RPC error.

• serverNotInitialized: Lean.JsonRpc.ErrorCode

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

• unknownErrorCode: Lean.JsonRpc.ErrorCode
• contentModified: Lean.JsonRpc.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: Lean.JsonRpc.ErrorCode

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

• rpcNeedsReconnect: Lean.JsonRpc.ErrorCode
• workerExited: Lean.JsonRpc.ErrorCode
• workerCrashed: Lean.JsonRpc.ErrorCode

Error codes defined by JSON-RPC and LSP.

instance Lean.JsonRpc.instInhabitedErrorCode : Inhabited Lean.JsonRpc.ErrorCode

instance Lean.JsonRpc.instBEqErrorCode : BEq Lean.JsonRpc.ErrorCode

instance Lean.JsonRpc.instFromJsonErrorCode : Lean.FromJson Lean.JsonRpc.ErrorCode

instance Lean.JsonRpc.instToJsonErrorCode : Lean.ToJson Lean.JsonRpc.ErrorCode

inductive Lean.JsonRpc.Message : Type

• request: Lean.JsonRpc.RequestID → String → Option Lean.Json.Structured → Lean.JsonRpc.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: String → Option Lean.Json.Structured → Lean.JsonRpc.Message

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

• response: Lean.JsonRpc.RequestID → Lean.Json → Lean.JsonRpc.Message

  A Response Message sent as a result of a request.

• responseError: Lean.JsonRpc.RequestID → Lean.JsonRpc.ErrorCode → String → Option Lean.Json → Lean.JsonRpc.Message

  A non-successful response.

A JSON-RPC message.

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

def Lean.JsonRpc.Batch : Type

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

• id : Lean.JsonRpc.RequestID
• method : String
• param : α

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

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

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

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

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

• method : String
• param : α

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.

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

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

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

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

• id : Lean.JsonRpc.RequestID
• result : α

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

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

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

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

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

• id : Lean.JsonRpc.RequestID
• code : Lean.JsonRpc.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.

Generic version of Message.responseError.

References:

• JSON-RPC
• LSP.

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

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

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

instance Lean.JsonRpc.instCoeStringRequestID : Coe String Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instCoeJsonNumberRequestID : Coe Lean.JsonNumber Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instLTRequestID : LT Lean.JsonRpc.RequestID

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

instance Lean.JsonRpc.instFromJsonRequestID : Lean.FromJson Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instToJsonRequestID : Lean.ToJson Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instToJsonMessage : Lean.ToJson Lean.JsonRpc.Message

instance Lean.JsonRpc.instFromJsonMessage : Lean.FromJson Lean.JsonRpc.Message

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

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

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

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

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

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

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

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

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

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

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