Documentation

Lean.Server.Completion.CompletionItemData

Used in CompletionItem.data?.

Instances For

    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.

    Instances For