Documentation

Lean.Server.Requests

Instances For
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline, reducible]
          abbrev Lean.Server.RequestTask (α : Type u_1) :
          Type u_1
          Equations
          Instances For
            @[inline, reducible]
            abbrev Lean.Server.RequestT (m : TypeType u_1) (α : Type) :
            Type u_1
            Equations
            Instances For
              @[inline, reducible]

              Workers execute request handlers in this monad.

              Equations
              Instances For
                @[inline, reducible]
                Equations
                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.
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Create a task which waits for the first snapshot matching p, handles various errors, and if a matching snapshot was found executes x with it. If not found, the task executes notFoundX.

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

                          Create a task which waits for the snapshot containing lspPos and executes f with it. If no such snapshot exists, the request fails with an error.

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

                                  The global request handlers table #

                                  We maintain a global map of LSP request handlers. This allows user code such as plugins to register its own handlers, for example to support ITP functionality such as goal state visualization.

                                  For details of how to register one, see registerLspRequestHandler.

                                  def Lean.Server.registerLspRequestHandler (method : String) (paramType : Type) [Lean.FromJson paramType] [Lean.Lsp.FileSource paramType] (respType : Type) [Lean.ToJson respType] (handler : paramTypeLean.Server.RequestM (Lean.Server.RequestTask respType)) :

                                  NB: This method may only be called in initialize blocks (user or builtin).

                                  A registration consists of:

                                  • a type of JSON-parsable request data paramType
                                  • a FileSource instance for it so the system knows where to route requests
                                  • a type of JSON-serializable response data respType
                                  • an actual handler which runs in the RequestM monad and is expected to produce an asynchronous RequestTask which does any waiting/computation

                                  A handler task may be cancelled at any time, so it should check the cancellation token when possible to handle this cooperatively. Any exceptions thrown in a request handler will be reported to the client as LSP error responses.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lean.Server.chainLspRequestHandler (method : String) (paramType : Type) [Lean.FromJson paramType] (respType : Type) [Lean.FromJson respType] [Lean.ToJson respType] (handler : paramTypeLean.Server.RequestTask respTypeLean.Server.RequestM (Lean.Server.RequestTask respType)) :

                                    NB: This method may only be called in initialize blocks (user or builtin).

                                    Register another handler to invoke after the last one registered for a method. At least one handler for the method must have already been registered to perform chaining.

                                    For more details on the registration of a handler, see registerLspRequestHandler.

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