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
    Equations
    Equations
    • One or more equations did not get rendered due to their size.

    Error codes defined by JSON-RPC and LSP.

    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.

      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
        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
          Equations
          • Lean.JsonRpc.instInhabitedRequest = { default := { id := default, method := default, param := default } }
          instance Lean.JsonRpc.instBEqRequest :
          {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Request α)
          Equations
          • Lean.JsonRpc.instBEqRequest = { beq := Lean.JsonRpc.beqRequest✝ }
          Equations
          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
            Equations
            • Lean.JsonRpc.instInhabitedNotification = { default := { method := default, param := default } }
            instance Lean.JsonRpc.instBEqNotification :
            {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Notification α)
            Equations
            • Lean.JsonRpc.instBEqNotification = { beq := Lean.JsonRpc.beqNotification✝ }
            Equations
            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
              Equations
              • Lean.JsonRpc.instInhabitedResponse = { default := { id := default, result := default } }
              instance Lean.JsonRpc.instBEqResponse :
              {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Response α)
              Equations
              • Lean.JsonRpc.instBEqResponse = { beq := Lean.JsonRpc.beqResponse✝ }
              Equations
              structure Lean.JsonRpc.ResponseError (α : Type u) :

              Generic version of Message.responseError.

              References:

              Instances For
                Equations
                • Lean.JsonRpc.instInhabitedResponseError = { default := { id := default, code := default, message := default, data? := default } }
                instance Lean.JsonRpc.instBEqResponseError :
                {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.ResponseError α)
                Equations
                • Lean.JsonRpc.instBEqResponseError = { beq := Lean.JsonRpc.beqResponseError✝ }
                Equations
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def IO.FS.Stream.readRequestAs (h : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def IO.FS.Stream.readNotificationAs (h : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For