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: Lake.Name → Lean.Lsp.RefIdent

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

• fvar: Lean.FVarId → Lean.Lsp.RefIdent

  Unnamed identifier. These are used for all local references.

instance Lean.Lsp.instBEqRefIdent : BEq Lean.Lsp.RefIdent

Equations

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

instance Lean.Lsp.instHashableRefIdent : Hashable Lean.Lsp.RefIdent

Equations

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

instance Lean.Lsp.instInhabitedRefIdent : Inhabited Lean.Lsp.RefIdent

Equations

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

def Lean.Lsp.RefIdent.toString : Lean.Lsp.RefIdent → String

Converts the reference identifier to a string by prefixing it with a symbol.

Equations

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

def Lean.Lsp.RefIdent.fromString (s : String) : Except String Lean.Lsp.RefIdent

Converts the string representation of a reference identifier back to a reference identifier. The string representation must have been created by RefIdent.toString.

Equations

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

instance Lean.Lsp.RefIdent.instFromJsonRefIdent : Lean.FromJson Lean.Lsp.RefIdent

Equations

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

instance Lean.Lsp.RefIdent.instToJsonRefIdent : Lean.ToJson Lean.Lsp.RefIdent

Equations

• Lean.Lsp.RefIdent.instToJsonRefIdent = { toJson := fun (ident : Lean.Lsp.RefIdent) => Lean.Json.str (Lean.Lsp.RefIdent.toString ident) }

structure Lean.Lsp.RefInfo.ParentDecl : Type

Information about the declaration surrounding a reference.

• name : Lake.Name

  Name of the declaration surrounding a reference.

• range : Lean.Lsp.Range

  Range of the declaration surrounding a reference.

• selectionRange : Lean.Lsp.Range

  Selection range of the declaration surrounding a reference.

instance Lean.Lsp.RefInfo.instToJsonParentDecl : Lean.ToJson Lean.Lsp.RefInfo.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 : Lean.Lsp.Range

  Range of the reference.

• parentDecl? : Option Lean.Lsp.RefInfo.ParentDecl

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

structure Lean.Lsp.RefInfo : Type

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

• definition? : Option Lean.Lsp.RefInfo.Location

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

• usages : Array Lean.Lsp.RefInfo.Location

  Usage sites of the reference.

instance Lean.Lsp.instToJsonRefInfo : Lean.ToJson Lean.Lsp.RefInfo

Equations

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

instance Lean.Lsp.instFromJsonRefInfo : Lean.FromJson Lean.Lsp.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 = Lean.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefInfo

instance Lean.Lsp.instToJsonModuleRefs : Lean.ToJson Lean.Lsp.ModuleRefs

Equations

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

instance Lean.Lsp.instFromJsonModuleRefs : Lean.FromJson Lean.Lsp.ModuleRefs

Equations

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

structure Lean.Lsp.LeanIleanInfoParams : Type

$/lean/ileanInfoUpdate and $/lean/ileanInfoFinal watchdog<-worker notifications.

Contains the file's definitions and references.

• version : Nat

  Version of the file these references are from.

• references : Lean.Lsp.ModuleRefs

  All references for the file.

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : Lean.FromJson Lean.Lsp.LeanIleanInfoParams

Equations

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

instance Lean.Lsp.instToJsonLeanIleanInfoParams : Lean.ToJson Lean.Lsp.LeanIleanInfoParams

Equations

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