inductive Lean.Lsp.CompletionIdentifier : Type

Identifier that is sent from the server to the client as part of the CompletionItem.data? field. Needed to resolve the CompletionItem when the client sends a completionItem/resolve request for that item, again containing the data? field provided by the server.

• const: Lake.Name → Lean.Lsp.CompletionIdentifier
• fvar: Lean.FVarId → Lean.Lsp.CompletionIdentifier

instance Lean.Lsp.instFromJsonCompletionIdentifier : Lean.FromJson Lean.Lsp.CompletionIdentifier

Equations

• Lean.Lsp.instFromJsonCompletionIdentifier = { fromJson? := Lean.Lsp.fromJsonCompletionIdentifier✝ }

instance Lean.Lsp.instToJsonCompletionIdentifier : Lean.ToJson Lean.Lsp.CompletionIdentifier

Equations

• Lean.Lsp.instToJsonCompletionIdentifier = { toJson := Lean.Lsp.toJsonCompletionIdentifier✝ }

structure Lean.Lsp.CompletionItemDataWithIdextends Lean.Lsp.CompletionItemData : Type

CompletionItemData that also contains a CompletionIdentifier. See the documentation ofCompletionItemData and CompletionIdentifier.

• params : Lean.Lsp.CompletionParams
• id? : Option Lean.Lsp.CompletionIdentifier

instance Lean.Lsp.instFromJsonCompletionItemDataWithId : Lean.FromJson Lean.Lsp.CompletionItemDataWithId

Equations

• Lean.Lsp.instFromJsonCompletionItemDataWithId = { fromJson? := Lean.Lsp.fromJsonCompletionItemDataWithId✝ }

instance Lean.Lsp.instToJsonCompletionItemDataWithId : Lean.ToJson Lean.Lsp.CompletionItemDataWithId

Equations

• Lean.Lsp.instToJsonCompletionItemDataWithId = { toJson := Lean.Lsp.toJsonCompletionItemDataWithId✝ }

def Lean.Lsp.CompletionItem.resolve (item : Lean.Lsp.CompletionItem) (id : Lean.Lsp.CompletionIdentifier) : Lean.MetaM Lean.Lsp.CompletionItem

Fills the CompletionItem.detail? field of item using the pretty-printed type identified by id.

Equations

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

opaque Lean.Server.Completion.eligibleHeaderDeclsRef : IO.Ref (Lean.HashMap Lake.Name Lean.ConstantInfo)

Cached header declarations for which allowCompletion headerEnv decl is true.

def Lean.Server.Completion.fillEligibleHeaderDecls (headerEnv : Lean.Environment) : IO Unit

Caches the declarations in the header for which allowCompletion headerEnv decl is true.

Equations

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

structure Lean.Server.Completion.State : Type

Intermediate state while completions are being computed.

• items : Array (Lean.Lsp.CompletionItem × Float)

  All completion items and their fuzzy match scores so far.

@[inline, reducible]

abbrev Lean.Server.Completion.M (α : Type) : Type

Monad used for completion computation that allows modifying a completion State and reading CompletionParams.

Equations

• Lean.Server.Completion.M = OptionT (ReaderT Lean.Lsp.CompletionParams (StateRefT' IO.RealWorld Lean.Server.Completion.State Lean.MetaM))

inductive Lean.Server.Completion.HoverInfo : Type

• after: Lean.Server.Completion.HoverInfo
• inside: Nat → Lean.Server.Completion.HoverInfo

def Lean.Server.Completion.matchNamespace (ns : Lake.Name) (nsFragment : Lake.Name) (danglingDot : Bool) : Option Float

Equations

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

def Lean.Server.Completion.completeNamespaces (ctx : Lean.Elab.ContextInfo) (id : Lake.Name) (danglingDot : Bool) : Lean.Server.Completion.M Unit

Equations

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

def Lean.Server.Completion.completeNamespaces.visitNamespaces (id : Lake.Name) (danglingDot : Bool) (add : Lake.Name → Lake.Name → Float → Lean.Server.Completion.M Unit) (ns : Lake.Name) (ns' : Lake.Name) : Lean.Server.Completion.M Unit

Equations

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

partial def Lean.Server.Completion.cmpModPrivate (n₁ : Lake.Name) (n₂ : Lake.Name) : Ordering

Compares n₁ and n₂ modulo private prefixes. Similar to Name.cmp but ignores all private prefixes in both names. Necessary because the namespaces of private names do not contain private prefixes.

def Lean.Server.Completion.NameSetModPrivate : Type

NameSet where names are compared according to cmpModPrivate. Helps speed up dot completion because it allows us to look up names without first having to strip the private prefix from deep in the name, letting us reject most names without having to scan the full name first.

Equations

• Lean.Server.Completion.NameSetModPrivate = Lean.RBTree Lake.Name Lean.Server.Completion.cmpModPrivate

def Lean.Server.Completion.find? (params : Lean.Lsp.CompletionParams) (fileMap : Lean.FileMap) (hoverPos : String.Pos) (infoTree : Lean.Elab.InfoTree) (caps : Lean.Lsp.ClientCapabilities) : IO (Option Lean.Lsp.CompletionList)

Equations

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

def Lean.Server.Completion.resolveCompletionItem? (fileMap : Lean.FileMap) (hoverPos : String.Pos) (infoTree : Lean.Elab.InfoTree) (item : Lean.Lsp.CompletionItem) (id : Lean.Lsp.CompletionIdentifier) : IO Lean.Lsp.CompletionItem

Fills the CompletionItem.detail? field of item using the pretty-printed type identified by id in the context found at hoverPos in infoTree.

Equations

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