structure Lean.Lsp.CompletionItemData : Type

Used in CompletionItem.data?.

• params : CompletionParams

instance Lean.Lsp.instFromJsonCompletionItemData : FromJson CompletionItemData

Equations

• Lean.Lsp.instFromJsonCompletionItemData = { fromJson? := Lean.Lsp.fromJsonCompletionItemData✝ }

instance Lean.Lsp.instToJsonCompletionItemData : ToJson CompletionItemData

Equations

• Lean.Lsp.instToJsonCompletionItemData = { toJson := Lean.Lsp.toJsonCompletionItemData✝ }

def Lean.Lsp.CompletionItem.getFileSource! (item : CompletionItem) : DocumentUri

Yields the file source of item by attempting to parse item.data? to CompletionItemData and obtaining the original file source from its params fields. Panics if item.data? is not present or cannot be parsed to CompletionItemData. Used when completionItem/resolve requests pass the watchdog to decide which file worker to forward the request to. Since this function can panic and clients typically send completionItem/resolve requests for every selected completion item, all completion items returned by the server in textDocument/completion requests must have a data? field that can be parsed to CompletionItemData.

Equations

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

instance Lean.Lsp.instFileSourceCompletionItem : FileSource CompletionItem

Equations

• Lean.Lsp.instFileSourceCompletionItem = { fileSource := Lean.Lsp.CompletionItem.getFileSource! }