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

def Lean.Lsp.instInhabitedImportInfo.default : 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.

def Lean.Lsp.instBEqRefIdent.beq : RefIdent → RefIdent → Bool

instance Lean.Lsp.instBEqRefIdent : BEq RefIdent

instance Lean.Lsp.instHashableRefIdent : Hashable RefIdent

def Lean.Lsp.instHashableRefIdent.hash : RefIdent → UInt64

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

def Lean.Lsp.instInhabitedRefIdent.default : RefIdent

def Lean.Lsp.instOrdRefIdent.ord : RefIdent → RefIdent → Ordering

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.

def Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr.fromJson : Json → Except String RefIdentJsonRepr

instance Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr : FromJson RefIdentJsonRepr

instance Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : ToJson RefIdentJsonRepr

def Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr.toJson : RefIdentJsonRepr → Json

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.DeclInfo : Type

Position information for a declaration. Inlined to reduce memory consumption.

• rangeStartPosLine : Nat

  Start line of range.

• rangeStartPosCharacter : Nat

  Start character of range.

• rangeEndPosLine : Nat

  End line of range.

• rangeEndPosCharacter : Nat

  End character of range.

• selectionRangeStartPosLine : Nat

  Start line of selection range.

• selectionRangeStartPosCharacter : Nat

  Start character of selection range.

• selectionRangeEndPosLine : Nat

  End line of selection range.

• selectionRangeEndPosCharacter : Nat

  End character of selection range.

def Lean.Lsp.DeclInfo.ofDeclarationRanges (r : DeclarationRanges) : DeclInfo

Converts a set of DeclarationRanges to a DeclInfo.

def Lean.Lsp.DeclInfo.range (i : DeclInfo) : Range

Range of this parent decl.

def Lean.Lsp.DeclInfo.selectionRange (i : DeclInfo) : Range

Selection range of this parent decl.

instance Lean.Lsp.instToJsonDeclInfo : ToJson DeclInfo

instance Lean.Lsp.instFromJsonDeclInfo : FromJson DeclInfo

def Lean.Lsp.Decls : Type

Declarations of a file with associated position information.

instance Lean.Lsp.instEmptyCollectionDecls : EmptyCollection Decls

instance Lean.Lsp.instForInIdDeclsProdStringDeclInfo : ForIn Id Decls (String × DeclInfo)

instance Lean.Lsp.instToJsonDecls : ToJson Decls

instance Lean.Lsp.instFromJsonDecls : FromJson Decls

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. The position information is inlined to reduce memory consumption.

• mk' :: (
• startPosLine : Nat

  Start line of the range of this location.

• startPosCharacter : Nat

  Start character of the range of this location.

• endPosLine : Nat

  End line of the range of this location.

• endPosCharacter : Nat

  End character of the range of this location.

• parentDecl : String

  Parent declaration of the reference. Empty string if the reference is itself a declaration. We do not use Option for memory consumption reasons.

• )

instance Lean.Lsp.RefInfo.instInhabitedLocation : Inhabited Location

def Lean.Lsp.RefInfo.instInhabitedLocation.default : Location

def Lean.Lsp.RefInfo.Location.mk (range : Range) (parentDecl? : Option String) : Location

Creates a RefInfo.Location.

def Lean.Lsp.RefInfo.Location.range (l : Location) : Range

Range of this location.

def Lean.Lsp.RefInfo.Location.parentDecl? (l : Location) : Option String

Name of the parent declaration of this 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.instEmptyCollectionModuleRefs : EmptyCollection ModuleRefs

instance Lean.Lsp.instForInModuleRefsProdRefIdentRefInfoOfMonad {m : Type u_1 → Type u_2} [Monad m] : 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

def Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams.fromJson : Json → Except String LeanILeanHeaderInfoParams

instance Lean.Lsp.instToJsonLeanILeanHeaderInfoParams : ToJson LeanILeanHeaderInfoParams

def Lean.Lsp.instToJsonLeanILeanHeaderInfoParams.toJson : LeanILeanHeaderInfoParams → Json

structure Lean.Lsp.LeanILeanHeaderSetupInfoParams : Type

Used in the $/lean/ileanHeaderSetupInfo watchdog <- worker notifications. Contains status information about lake setup-file.

• version : Nat

  Version of the file these imports are from.

• isSetupFailure : Bool

  Whether setting up the header using lake setup-file has failed.

def Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams.fromJson : Json → Except String LeanILeanHeaderSetupInfoParams

instance Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams : FromJson LeanILeanHeaderSetupInfoParams

instance Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams : ToJson LeanILeanHeaderSetupInfoParams

def Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams.toJson : LeanILeanHeaderSetupInfoParams → Json

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.

• decls : Decls

  All decls for the file.

def Lean.Lsp.instFromJsonLeanIleanInfoParams.fromJson : Json → Except String LeanIleanInfoParams

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : FromJson LeanIleanInfoParams

def Lean.Lsp.instToJsonLeanIleanInfoParams.toJson : LeanIleanInfoParams → Json

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

def Lean.Lsp.instFromJsonLeanImportClosureParams.fromJson : Json → Except String LeanImportClosureParams

instance Lean.Lsp.instToJsonLeanImportClosureParams : ToJson LeanImportClosureParams

def Lean.Lsp.instToJsonLeanImportClosureParams.toJson : LeanImportClosureParams → Json

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

def Lean.Lsp.instFromJsonLeanStaleDependencyParams.fromJson : Json → Except String LeanStaleDependencyParams

def Lean.Lsp.instToJsonLeanStaleDependencyParams.toJson : LeanStaleDependencyParams → Json

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.

def Lean.Lsp.instFromJsonOpenNamespace.fromJson : Json → Except String OpenNamespace

instance Lean.Lsp.instFromJsonOpenNamespace : FromJson OpenNamespace

instance Lean.Lsp.instToJsonOpenNamespace : ToJson OpenNamespace

def Lean.Lsp.instToJsonOpenNamespace.toJson : OpenNamespace → Json

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

def Lean.Lsp.instFromJsonLeanModuleQuery.fromJson : Json → Except String LeanModuleQuery

def Lean.Lsp.instToJsonLeanModuleQuery.toJson : LeanModuleQuery → Json

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

def Lean.Lsp.instFromJsonLeanQueryModuleParams.fromJson : Json → Except String LeanQueryModuleParams

def Lean.Lsp.instToJsonLeanQueryModuleParams.toJson : LeanQueryModuleParams → Json

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.

def Lean.Lsp.instFromJsonLeanIdentifier.fromJson : Json → Except String LeanIdentifier

instance Lean.Lsp.instFromJsonLeanIdentifier : FromJson LeanIdentifier

def Lean.Lsp.instToJsonLeanIdentifier.toJson : LeanIdentifier → Json

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.

def Lean.Lsp.instFromJsonLeanQueryModuleResponse.fromJson : Json → Except String LeanQueryModuleResponse

instance Lean.Lsp.instFromJsonLeanQueryModuleResponse : FromJson LeanQueryModuleResponse

def Lean.Lsp.instToJsonLeanQueryModuleResponse.toJson : LeanQueryModuleResponse → Json

instance Lean.Lsp.instToJsonLeanQueryModuleResponse : ToJson LeanQueryModuleResponse

def Lean.Lsp.instInhabitedLeanQueryModuleResponse.default : LeanQueryModuleResponse

instance Lean.Lsp.instInhabitedLeanQueryModuleResponse : Inhabited LeanQueryModuleResponse

structure Lean.Lsp.LeanDeclIdent : Type

Name of a declaration in a given module.

• module : Name

  Name of the module that this identifier is in.

• decl : Name

  Name of the declaration.

def Lean.Lsp.instFromJsonLeanDeclIdent.fromJson : Json → Except String LeanDeclIdent

instance Lean.Lsp.instFromJsonLeanDeclIdent : FromJson LeanDeclIdent

instance Lean.Lsp.instToJsonLeanDeclIdent : ToJson LeanDeclIdent

def Lean.Lsp.instToJsonLeanDeclIdent.toJson : LeanDeclIdent → Json

structure Lean.Lsp.LeanLocationLinkextends Lean.Lsp.LocationLink : Type

LocationLink with additional meta-data that allows the watchdog to resolve the range of this LocationLink. This is necessary because the position information from the .olean may be stale (e.g. if the user has edited the file that the definition is from, but neither saved or built it), while file workers sync their current reference information into the watchdog using ilean info notifications, which is up-to-date.

• originSelectionRange? : Option Range
• targetUri : DocumentUri
• targetRange : Range
• targetSelectionRange : Range
• ident? : Option LeanDeclIdent

  Identifier that caused this location link.

• isDefault : Bool

  Whether this location link was generated by a fallback handler. If the file worker can't produce any non-fallback location links, the watchdog tries again using its reference information from the ileans and ilean updates.

def Lean.Lsp.instFromJsonLeanLocationLink.fromJson : Json → Except String LeanLocationLink

instance Lean.Lsp.instFromJsonLeanLocationLink : FromJson LeanLocationLink

def Lean.Lsp.instToJsonLeanLocationLink.toJson : LeanLocationLink → Json

instance Lean.Lsp.instToJsonLeanLocationLink : ToJson LeanLocationLink