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.

@[implicit_reducible]

instance Lean.Lsp.instInhabitedImportInfo : Inhabited ImportInfo

def Lean.Lsp.instInhabitedImportInfo.default : ImportInfo

@[implicit_reducible]

instance Lean.Lsp.instToJsonImportInfo : ToJson ImportInfo

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instBEqRefIdent : BEq RefIdent

@[implicit_reducible]

instance Lean.Lsp.instHashableRefIdent : Hashable RefIdent

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

def Lean.Lsp.instInhabitedRefIdent.default : RefIdent

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr : FromJson RefIdentJsonRepr

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.RefIdent.instFromJson : FromJson RefIdent

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instToJsonDeclInfo : ToJson DeclInfo

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDeclInfo : FromJson DeclInfo

def Lean.Lsp.Decls : Type

Declarations of a file with associated position information.

@[implicit_reducible]

instance Lean.Lsp.instEmptyCollectionDecls : EmptyCollection Decls

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDecls : ToJson Decls

@[implicit_reducible]

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.

• )

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instToJsonRefInfo : ToJson RefInfo

@[implicit_reducible]

instance Lean.Lsp.instFromJsonRefInfo : FromJson RefInfo

def Lean.Lsp.ModuleRefs : Type

References from a single module/file

@[implicit_reducible]

instance Lean.Lsp.instEmptyCollectionModuleRefs : EmptyCollection ModuleRefs

@[implicit_reducible]

instance Lean.Lsp.instForInModuleRefsProdRefIdentRefInfoOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m ModuleRefs (RefIdent × RefInfo)

@[implicit_reducible]

instance Lean.Lsp.instToJsonModuleRefs : ToJson ModuleRefs

@[implicit_reducible]

instance Lean.Lsp.instFromJsonModuleRefs : FromJson ModuleRefs

structure Lean.Lsp.LeanILeanHeaderSetupInfoParams : Type

Used in the $/lean/ileanHeaderSetupInfo watchdog <- worker notifications. Contains status information about lake setup-file and the direct imports of the file managed by a worker.

• version : Nat

  Version of the file these imports are from.

• isSetupFailure : Bool

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

• directImports : Array ImportInfo

  Direct imports of this file.

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams : FromJson LeanILeanHeaderSetupInfoParams

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : FromJson LeanIleanInfoParams

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanImportClosureParams : FromJson LeanImportClosureParams

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

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

@[implicit_reducible]

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.

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanStaleDependencyParams : FromJson LeanStaleDependencyParams

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonOpenNamespace : FromJson OpenNamespace

@[implicit_reducible]

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.

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanModuleQuery : FromJson LeanModuleQuery

@[implicit_reducible]

instance Lean.Lsp.instToJsonLeanModuleQuery : ToJson LeanModuleQuery

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

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanQueryModuleParams : FromJson LeanQueryModuleParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonLeanQueryModuleParams : ToJson LeanQueryModuleParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanIdentifier : FromJson LeanIdentifier

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanQueryModuleResponse : FromJson LeanQueryModuleResponse

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonLeanQueryModuleResponse : ToJson LeanQueryModuleResponse

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

def Lean.Lsp.instInhabitedLeanQueryModuleResponse.default : LeanQueryModuleResponse

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanDeclIdent : FromJson LeanDeclIdent

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanLocationLink : FromJson LeanLocationLink

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonLeanLocationLink : ToJson LeanLocationLink