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.

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

Equations

• Lean.Lsp.instBEqRefIdent = { beq := Lean.Lsp.beqRefIdent✝ }

instance Lean.Lsp.instHashableRefIdent : Hashable RefIdent

Equations

• Lean.Lsp.instHashableRefIdent = { hash := Lean.Lsp.hashRefIdent✝ }

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

Equations

• Lean.Lsp.instInhabitedRefIdent = { default := Lean.Lsp.RefIdent.const default default }

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

Equations

• Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr = { fromJson? := Lean.Lsp.RefIdent.fromJsonRefIdentJsonRepr✝ }

instance Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : ToJson RefIdentJsonRepr

Equations

• Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr = { toJson := Lean.Lsp.RefIdent.toJsonRefIdentJsonRepr✝ }

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

Converts id to its compact serialization representation.

Equations

• (Lean.Lsp.RefIdent.const a a_1).toJsonRepr = Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1
• (Lean.Lsp.RefIdent.fvar a a_1).toJsonRepr = Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1

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

Converts repr to RefIdent.

Equations

• Lean.Lsp.RefIdent.fromJsonRepr (Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1) = Lean.Lsp.RefIdent.const a a_1
• Lean.Lsp.RefIdent.fromJsonRepr (Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1) = Lean.Lsp.RefIdent.fvar a a_1

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

Converts RefIdent from a JSON for RefIdentJsonRepr.

Equations

• Lean.Lsp.RefIdent.fromJson? s = do let __do_lift ← Lean.fromJson? s pure (Lean.Lsp.RefIdent.fromJsonRepr __do_lift)

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

Converts RefIdent to a JSON for RefIdentJsonRepr.

Equations

• id.toJson = Lean.toJson id.toJsonRepr

instance Lean.Lsp.RefIdent.instFromJson : FromJson RefIdent

Equations

• Lean.Lsp.RefIdent.instFromJson = { fromJson? := Lean.Lsp.RefIdent.fromJson? }

instance Lean.Lsp.RefIdent.instToJson : ToJson RefIdent

Equations

• Lean.Lsp.RefIdent.instToJson = { toJson := Lean.Lsp.RefIdent.toJson }

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

Equations

• Lean.Lsp.RefInfo.instToJsonParentDecl = { toJson := Lean.Lsp.RefInfo.toJsonParentDecl✝ }

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

Equations

• Lean.Lsp.RefInfo.instInhabitedLocation = { default := { range := default, parentDecl? := default } }

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

Equations

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

instance Lean.Lsp.instFromJsonRefInfo : FromJson RefInfo

Equations

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

def Lean.Lsp.ModuleRefs : Type

References from a single module/file

Equations

• Lean.Lsp.ModuleRefs = Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefInfo

instance Lean.Lsp.instToJsonModuleRefs : ToJson ModuleRefs

Equations

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

instance Lean.Lsp.instFromJsonModuleRefs : FromJson ModuleRefs

Equations

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

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

Equations

• Lean.Lsp.instFromJsonLeanIleanInfoParams = { fromJson? := Lean.Lsp.fromJsonLeanIleanInfoParams✝ }

instance Lean.Lsp.instToJsonLeanIleanInfoParams : ToJson LeanIleanInfoParams

Equations

• Lean.Lsp.instToJsonLeanIleanInfoParams = { toJson := Lean.Lsp.toJsonLeanIleanInfoParams✝ }

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

Equations

• Lean.Lsp.instFromJsonLeanImportClosureParams = { fromJson? := Lean.Lsp.fromJsonLeanImportClosureParams✝ }

instance Lean.Lsp.instToJsonLeanImportClosureParams : ToJson LeanImportClosureParams

Equations

• Lean.Lsp.instToJsonLeanImportClosureParams = { toJson := Lean.Lsp.toJsonLeanImportClosureParams✝ }

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

Equations

• Lean.Lsp.instFromJsonLeanStaleDependencyParams = { fromJson? := Lean.Lsp.fromJsonLeanStaleDependencyParams✝ }

instance Lean.Lsp.instToJsonLeanStaleDependencyParams : ToJson LeanStaleDependencyParams

Equations

• Lean.Lsp.instToJsonLeanStaleDependencyParams = { toJson := Lean.Lsp.toJsonLeanStaleDependencyParams✝ }