Documentation

Lean.Data.JsonRpc

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

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.

Instances For

    Error codes defined by JSON-RPC and LSP.

    Instances For

      A JSON-RPC message.

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

      Instances For
        Instances For
          structure Lean.JsonRpc.Request (α : 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.

          Instances For
            instance Lean.JsonRpc.instBEqRequest :
            {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Request α)
            structure Lean.JsonRpc.Notification (α : Type u) :

            Generic version of Message.notification.

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

            Instances For
              instance Lean.JsonRpc.instBEqNotification :
              {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Notification α)
              structure Lean.JsonRpc.Response (α : 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:

              Instances For
                instance Lean.JsonRpc.instBEqResponse :
                {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Response α)
                structure Lean.JsonRpc.ResponseError (α : Type u) :

                Generic version of Message.responseError.

                References:

                Instances For
                  instance Lean.JsonRpc.instBEqResponseError :
                  {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.ResponseError α)
                  def IO.FS.Stream.readRequestAs (h : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] :
                  Instances For
                    def IO.FS.Stream.readNotificationAs (h : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] :
                    Instances For