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.

structure Lean.Lsp.ImportInfo : Type

Information about a single import statement.

• module : String

  Name of the module that is imported.

• isPrivate : Bool

  Whether the module is being imported via private import.

• isAll : Bool

  Whether the module is being imported via import all.

• isMeta : Bool

  Whether the module is being imported via meta import.

instance Lean.Lsp.instInhabitedImportInfo : Inhabited ImportInfo

instance Lean.Lsp.instToJsonImportInfo : ToJson ImportInfo

instance Lean.Lsp.instFromJsonImportInfo : FromJson ImportInfo

inductive Lean.Lsp.RefIdent : Type

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.

instance Lean.Lsp.instBEqRefIdent : BEq RefIdent

instance Lean.Lsp.instHashableRefIdent : Hashable RefIdent

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

instance Lean.Lsp.instOrdRefIdent : Ord RefIdent

inductive Lean.Lsp.RefIdent.RefIdentJsonRepr : Type

Shortened representation of RefIdent for more compact serialization.

• c (m n : String) : RefIdentJsonRepr

  Shortened representation of RefIdent.const for more compact serialization.

• f (m i : String) : RefIdentJsonRepr

  Shortened representation of RefIdent.fvar for more compact serialization.

instance Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr : FromJson RefIdentJsonRepr

instance Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : ToJson RefIdentJsonRepr

def Lean.Lsp.RefIdent.toJsonRepr (id : RefIdent) : RefIdentJsonRepr

Converts id to its compact serialization representation.

def Lean.Lsp.RefIdent.fromJsonRepr (repr : RefIdentJsonRepr) : RefIdent

Converts repr to RefIdent.

def Lean.Lsp.RefIdent.fromJson? (s : Json) : Except String RefIdent

Converts RefIdent from a JSON for RefIdentJsonRepr.

def Lean.Lsp.RefIdent.toJson (id : RefIdent) : Json

Converts RefIdent to a JSON for RefIdentJsonRepr.

instance Lean.Lsp.RefIdent.instFromJson : FromJson RefIdent

instance Lean.Lsp.RefIdent.instToJson : ToJson RefIdent

structure Lean.Lsp.RefInfo.ParentDecl : Type

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.

instance Lean.Lsp.RefInfo.instToJsonParentDecl : ToJson ParentDecl

structure Lean.Lsp.RefInfo.Location : Type

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.

instance Lean.Lsp.RefInfo.instInhabitedLocation : Inhabited Location

structure Lean.Lsp.RefInfo : Type

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.

instance Lean.Lsp.instToJsonRefInfo : ToJson RefInfo

instance Lean.Lsp.instFromJsonRefInfo : FromJson RefInfo

def Lean.Lsp.ModuleRefs : Type

References from a single module/file

instance Lean.Lsp.instModuleRefsEmptyCollection : EmptyCollection ModuleRefs

instance Lean.Lsp.instForInModuleRefsProdRefIdentRefInfo {m : Type u_1 → Type u_2} : ForIn m ModuleRefs (RefIdent × RefInfo)

instance Lean.Lsp.instToJsonModuleRefs : ToJson ModuleRefs

instance Lean.Lsp.instFromJsonModuleRefs : FromJson ModuleRefs

structure Lean.Lsp.LeanILeanHeaderInfoParams : Type

Used in the $/lean/ileanHeaderInfo watchdog <- worker notifications. Contains the direct imports of the file managed by a worker.

• version : Nat

  Version of the file these imports are from.

• directImports : Array ImportInfo

  Direct imports of this file.

instance Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams : FromJson LeanILeanHeaderInfoParams

instance Lean.Lsp.instToJsonLeanILeanHeaderInfoParams : ToJson LeanILeanHeaderInfoParams

structure Lean.Lsp.LeanIleanInfoParams : Type

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.

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : FromJson LeanIleanInfoParams

instance Lean.Lsp.instToJsonLeanIleanInfoParams : ToJson LeanIleanInfoParams

structure Lean.Lsp.LeanImportClosureParams : Type

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

• importClosure : Array DocumentUri

  Full import closure of the file.

instance Lean.Lsp.instFromJsonLeanImportClosureParams : FromJson LeanImportClosureParams

instance Lean.Lsp.instToJsonLeanImportClosureParams : ToJson LeanImportClosureParams

structure Lean.Lsp.LeanStaleDependencyParams : Type

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.

instance Lean.Lsp.instFromJsonLeanStaleDependencyParams : FromJson LeanStaleDependencyParams

instance Lean.Lsp.instToJsonLeanStaleDependencyParams : ToJson LeanStaleDependencyParams

inductive Lean.Lsp.OpenNamespace : Type

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.

instance Lean.Lsp.instFromJsonOpenNamespace : FromJson OpenNamespace

instance Lean.Lsp.instToJsonOpenNamespace : ToJson OpenNamespace

structure Lean.Lsp.LeanModuleQuery : Type

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.

instance Lean.Lsp.instFromJsonLeanModuleQuery : FromJson LeanModuleQuery

instance Lean.Lsp.instToJsonLeanModuleQuery : ToJson LeanModuleQuery

structure Lean.Lsp.LeanQueryModuleParams : Type

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.

• queries : Array LeanModuleQuery

  Module queries for extracting .ilean information in the watchdog.

instance Lean.Lsp.instFromJsonLeanQueryModuleParams : FromJson LeanQueryModuleParams

instance Lean.Lsp.instToJsonLeanQueryModuleParams : ToJson LeanQueryModuleParams

structure Lean.Lsp.LeanIdentifier : Type

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.

instance Lean.Lsp.instFromJsonLeanIdentifier : FromJson LeanIdentifier

instance Lean.Lsp.instToJsonLeanIdentifier : ToJson LeanIdentifier

@[reducible, inline]

abbrev Lean.Lsp.LeanQueriedModule : Type

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

structure Lean.Lsp.LeanQueryModuleResponse : Type

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

• queryResults : Array LeanQueriedModule

  Results for each query in LeanQueryModuleParams. Positions correspond to queries in the parameter of the request.

instance Lean.Lsp.instFromJsonLeanQueryModuleResponse : FromJson LeanQueryModuleResponse

instance Lean.Lsp.instToJsonLeanQueryModuleResponse : ToJson LeanQueryModuleResponse

instance Lean.Lsp.instInhabitedLeanQueryModuleResponse : Inhabited LeanQueryModuleResponse