inductive Lean.Lsp.FileIdent : Type

• uri (uri : DocumentUri) : FileIdent
• mod (mod : Name) : FileIdent

instance Lean.Lsp.instInhabitedFileIdent : Inhabited FileIdent

def Lean.Lsp.instInhabitedFileIdent.default : FileIdent

instance Lean.Lsp.instToStringFileIdent : ToString FileIdent

class Lean.Lsp.FileSource (α : Type) : Type

• fileSource : α → FileIdent

instance Lean.Lsp.instFileSourceLocation : FileSource Location

instance Lean.Lsp.instFileSourceTextDocumentIdentifier : FileSource TextDocumentIdentifier

instance Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier : FileSource VersionedTextDocumentIdentifier

instance Lean.Lsp.instFileSourceTextDocumentEdit : FileSource TextDocumentEdit

instance Lean.Lsp.instFileSourceTextDocumentItem : FileSource TextDocumentItem

instance Lean.Lsp.instFileSourceTextDocumentPositionParams : FileSource TextDocumentPositionParams

instance Lean.Lsp.instFileSourceDidOpenTextDocumentParams : FileSource DidOpenTextDocumentParams

instance Lean.Lsp.instFileSourceDidChangeTextDocumentParams : FileSource DidChangeTextDocumentParams

instance Lean.Lsp.instFileSourceDidSaveTextDocumentParams : FileSource DidSaveTextDocumentParams

instance Lean.Lsp.instFileSourceDidCloseTextDocumentParams : FileSource DidCloseTextDocumentParams

instance Lean.Lsp.instFileSourceCompletionParams : FileSource CompletionParams

instance Lean.Lsp.instFileSourceHoverParams : FileSource HoverParams

instance Lean.Lsp.instFileSourceDeclarationParams : FileSource DeclarationParams

instance Lean.Lsp.instFileSourceDefinitionParams : FileSource DefinitionParams

instance Lean.Lsp.instFileSourceTypeDefinitionParams : FileSource TypeDefinitionParams

instance Lean.Lsp.instFileSourceReferenceParams : FileSource ReferenceParams

instance Lean.Lsp.instFileSourceWaitForDiagnosticsParams : FileSource WaitForDiagnosticsParams

instance Lean.Lsp.instFileSourceDocumentHighlightParams : FileSource DocumentHighlightParams

instance Lean.Lsp.instFileSourceDocumentSymbolParams : FileSource DocumentSymbolParams

instance Lean.Lsp.instFileSourceSemanticTokensParams : FileSource SemanticTokensParams

instance Lean.Lsp.instFileSourceSemanticTokensRangeParams : FileSource SemanticTokensRangeParams

instance Lean.Lsp.instFileSourceFoldingRangeParams : FileSource FoldingRangeParams

instance Lean.Lsp.instFileSourcePlainGoalParams : FileSource PlainGoalParams

instance Lean.Lsp.instFileSourcePlainTermGoalParams : FileSource PlainTermGoalParams

instance Lean.Lsp.instFileSourceRpcConnectParams : FileSource RpcConnectParams

instance Lean.Lsp.instFileSourceRpcCallParams : FileSource RpcCallParams

instance Lean.Lsp.instFileSourceRpcReleaseParams : FileSource RpcReleaseParams

instance Lean.Lsp.instFileSourceRpcKeepAliveParams : FileSource RpcKeepAliveParams

instance Lean.Lsp.instFileSourceCodeActionParams : FileSource CodeActionParams

instance Lean.Lsp.instFileSourceInlayHintParams : FileSource InlayHintParams

instance Lean.Lsp.instFileSourceSignatureHelpParams : FileSource SignatureHelpParams

instance Lean.Lsp.instFileSourceDocumentColorParams : FileSource DocumentColorParams

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

Yields the file source of item by attempting to obtain mod : Name from item.data?.
Panics if item.data? is not present or does not contain a mod field and the first element of a data? array cannot be parsed to Name. 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 has a mod field.

instance Lean.Lsp.instFileSourceCompletionItem : FileSource CompletionItem