Documentation

Lean.Data.Lsp.Internal

This file contains types for communication between the watchdog and the workers. These messages are not visible externally to users of the LSP server.

Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON.

Identifier of a reference.

  • const (moduleName identName : String) : RefIdent

    Named identifier. These are used in all references that are globally available.

  • fvar (moduleName id : String) : RefIdent

    Unnamed identifier. These are used for all local references.

Instances For

    Shortened representation of RefIdent for more compact serialization.

    Instances For

      Converts id to its compact serialization representation.

      Equations
        Instances For

          Converts repr to RefIdent.

          Equations
            Instances For

              Converts RefIdent from a JSON for RefIdentJsonRepr.

              Equations
                Instances For

                  Converts RefIdent to a JSON for RefIdentJsonRepr.

                  Equations
                    Instances For

                      Information about the declaration surrounding a reference.

                      • name : String

                        Name of the declaration surrounding a reference.

                      • range : Range

                        Range of the declaration surrounding a reference.

                      • selectionRange : Range

                        Selection range of the declaration surrounding a reference.

                      Instances For

                        Denotes the range of a reference, as well as the parent declaration of the reference. If the reference is itself a declaration, then it contains no parent declaration.

                        • range : Range

                          Range of the reference.

                        • parentDecl? : Option ParentDecl

                          Parent declaration of the reference. none if the reference is itself a declaration.

                        Instances For

                          Definition site and usage sites of a reference. Obtained from Lean.Server.RefInfo.

                          • definition? : Option Location

                            Definition site of the reference. May be none when we cannot find a definition site.

                          • usages : Array Location

                            Usage sites of the reference.

                          Instances For

                            References from a single module/file

                            Equations
                              Instances For

                                Used in the $/lean/ileanInfoUpdate and $/lean/ileanInfoFinal watchdog <- worker notifications. Contains the definitions and references of the file managed by a worker.

                                • version : Nat

                                  Version of the file these references are from.

                                • references : ModuleRefs

                                  All references for the file.

                                Instances For

                                  Used in the $/lean/importClosure watchdog <- worker notification. Contains the full import closure of the file managed by a worker.

                                  Instances For

                                    Used in the $/lean/importClosure watchdog -> worker notification. Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.

                                    • staleDependency : DocumentUri

                                      The dependency that is stale.

                                    Instances For

                                      LSP type for Lean.OpenDecl.

                                      • allExcept («namespace» : Name) (exceptions : Array Name) : OpenNamespace

                                        All declarations in «namespace» are opened, except for exceptions.

                                      • renamed («from» to : Name) : OpenNamespace

                                        The declaration «from» is renamed to to.

                                      Instances For

                                        Query in the $/lean/queryModule watchdog <- worker request.

                                        • identifier : String

                                          Identifier (potentially partial) to query.

                                        • openNamespaces : Array OpenNamespace

                                          Namespaces that are open at the position of identifier. Used for accurately matching declarations against identifier in context.

                                        Instances For

                                          Used in the $/lean/queryModule watchdog <- worker request, which is used by the worker to extract information from the .ilean information in the watchdog.

                                          • sourceRequestID : JsonRpc.RequestID

                                            The request ID in the context of which this worker -> watchdog request was emitted. Used for cancelling this request in the watchdog.

                                          • Module queries for extracting .ilean information in the watchdog.

                                          Instances For

                                            Result entry of a module query.

                                            • module : Name

                                              Module that decl is defined in.

                                            • decl : Name

                                              Full name of the declaration that matches the query.

                                            • isExactMatch : Bool

                                              Whether this decl matched the query exactly.

                                            Instances For
                                              @[reducible, inline]

                                              Result for a single module query. Identifiers in the response are sorted descendingly by how well they match the query.

                                              Equations
                                                Instances For

                                                  Response for the $/lean/queryModule watchdog <- worker request.

                                                  Instances For