source
inductive Lean.Lsp.FileIdent :
Type

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

Instances For

source
instance Lean.Lsp.instInhabitedFileIdent :
Inhabited FileIdent
Equations

- Lean.Lsp.instInhabitedFileIdent = { default := Lean.Lsp.instInhabitedFileIdent.default }

source
def Lean.Lsp.instInhabitedFileIdent.default :
FileIdent
Equations

- Lean.Lsp.instInhabitedFileIdent.default = Lean.Lsp.FileIdent.uri default

Instances For

source
instance Lean.Lsp.instToStringFileIdent :
ToString FileIdent
Equations

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

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

- fileSource : α → FileIdent

Instances

source
instance Lean.Lsp.instFileSourceLocation :
FileSource Location
Equations

- Lean.Lsp.instFileSourceLocation = { fileSource := fun (l : Lean.Lsp.Location) => Lean.Lsp.FileIdent.uri l.uri }

source
instance Lean.Lsp.instFileSourceTextDocumentIdentifier :
FileSource TextDocumentIdentifier
Equations

- Lean.Lsp.instFileSourceTextDocumentIdentifier = { fileSource := fun (i : Lean.Lsp.TextDocumentIdentifier) => Lean.Lsp.FileIdent.uri i.uri }

source
instance Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier :
FileSource VersionedTextDocumentIdentifier
Equations

- Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier = { fileSource := fun (i : Lean.Lsp.VersionedTextDocumentIdentifier) => Lean.Lsp.FileIdent.uri i.uri }

source
instance Lean.Lsp.instFileSourceTextDocumentEdit :
FileSource TextDocumentEdit
Equations

- Lean.Lsp.instFileSourceTextDocumentEdit = { fileSource := fun (e : Lean.Lsp.TextDocumentEdit) => Lean.Lsp.fileSource e.textDocument }

source
instance Lean.Lsp.instFileSourceTextDocumentItem :
FileSource TextDocumentItem
Equations

- Lean.Lsp.instFileSourceTextDocumentItem = { fileSource := fun (i : Lean.Lsp.TextDocumentItem) => Lean.Lsp.FileIdent.uri i.uri }

source
instance Lean.Lsp.instFileSourceTextDocumentPositionParams :
FileSource TextDocumentPositionParams
Equations

- Lean.Lsp.instFileSourceTextDocumentPositionParams = { fileSource := fun (p : Lean.Lsp.TextDocumentPositionParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceDidOpenTextDocumentParams :
FileSource DidOpenTextDocumentParams
Equations

- Lean.Lsp.instFileSourceDidOpenTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidOpenTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceDidChangeTextDocumentParams :
FileSource DidChangeTextDocumentParams
Equations

- Lean.Lsp.instFileSourceDidChangeTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidChangeTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceDidSaveTextDocumentParams :
FileSource DidSaveTextDocumentParams
Equations

- Lean.Lsp.instFileSourceDidSaveTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidSaveTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceDidCloseTextDocumentParams :
FileSource DidCloseTextDocumentParams
Equations

- Lean.Lsp.instFileSourceDidCloseTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidCloseTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceCompletionParams :
FileSource CompletionParams
Equations

- Lean.Lsp.instFileSourceCompletionParams = { fileSource := fun (h : Lean.Lsp.CompletionParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceHoverParams :
FileSource HoverParams
Equations

- Lean.Lsp.instFileSourceHoverParams = { fileSource := fun (h : Lean.Lsp.HoverParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceDeclarationParams :
FileSource DeclarationParams
Equations

- Lean.Lsp.instFileSourceDeclarationParams = { fileSource := fun (h : Lean.Lsp.DeclarationParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceDefinitionParams :
FileSource DefinitionParams
Equations

- Lean.Lsp.instFileSourceDefinitionParams = { fileSource := fun (h : Lean.Lsp.DefinitionParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceTypeDefinitionParams :
FileSource TypeDefinitionParams
Equations

- Lean.Lsp.instFileSourceTypeDefinitionParams = { fileSource := fun (h : Lean.Lsp.TypeDefinitionParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceReferenceParams :
FileSource ReferenceParams
Equations

- Lean.Lsp.instFileSourceReferenceParams = { fileSource := fun (h : Lean.Lsp.ReferenceParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceWaitForDiagnosticsParams :
FileSource WaitForDiagnosticsParams
Equations

- Lean.Lsp.instFileSourceWaitForDiagnosticsParams = { fileSource := fun (p : Lean.Lsp.WaitForDiagnosticsParams) => Lean.Lsp.FileIdent.uri p.uri }

source
instance Lean.Lsp.instFileSourceDocumentHighlightParams :
FileSource DocumentHighlightParams
Equations

- Lean.Lsp.instFileSourceDocumentHighlightParams = { fileSource := fun (h : Lean.Lsp.DocumentHighlightParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }

source
instance Lean.Lsp.instFileSourceDocumentSymbolParams :
FileSource DocumentSymbolParams
Equations

- Lean.Lsp.instFileSourceDocumentSymbolParams = { fileSource := fun (p : Lean.Lsp.DocumentSymbolParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceSemanticTokensParams :
FileSource SemanticTokensParams
Equations

- Lean.Lsp.instFileSourceSemanticTokensParams = { fileSource := fun (p : Lean.Lsp.SemanticTokensParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceSemanticTokensRangeParams :
FileSource SemanticTokensRangeParams
Equations

- Lean.Lsp.instFileSourceSemanticTokensRangeParams = { fileSource := fun (p : Lean.Lsp.SemanticTokensRangeParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceFoldingRangeParams :
FileSource FoldingRangeParams
Equations

- Lean.Lsp.instFileSourceFoldingRangeParams = { fileSource := fun (p : Lean.Lsp.FoldingRangeParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourcePlainGoalParams :
FileSource PlainGoalParams
Equations

- Lean.Lsp.instFileSourcePlainGoalParams = { fileSource := fun (p : Lean.Lsp.PlainGoalParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourcePlainTermGoalParams :
FileSource PlainTermGoalParams
Equations

- Lean.Lsp.instFileSourcePlainTermGoalParams = { fileSource := fun (p : Lean.Lsp.PlainTermGoalParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceRpcConnectParams :
FileSource RpcConnectParams
Equations

- Lean.Lsp.instFileSourceRpcConnectParams = { fileSource := fun (p : Lean.Lsp.RpcConnectParams) => Lean.Lsp.FileIdent.uri p.uri }

source
instance Lean.Lsp.instFileSourceRpcCallParams :
FileSource RpcCallParams
Equations

- Lean.Lsp.instFileSourceRpcCallParams = { fileSource := fun (p : Lean.Lsp.RpcCallParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceRpcReleaseParams :
FileSource RpcReleaseParams
Equations

- Lean.Lsp.instFileSourceRpcReleaseParams = { fileSource := fun (p : Lean.Lsp.RpcReleaseParams) => Lean.Lsp.FileIdent.uri p.uri }

source
instance Lean.Lsp.instFileSourceRpcKeepAliveParams :
FileSource RpcKeepAliveParams
Equations

- Lean.Lsp.instFileSourceRpcKeepAliveParams = { fileSource := fun (p : Lean.Lsp.RpcKeepAliveParams) => Lean.Lsp.FileIdent.uri p.uri }

source
instance Lean.Lsp.instFileSourceCodeActionParams :
FileSource CodeActionParams
Equations

- Lean.Lsp.instFileSourceCodeActionParams = { fileSource := fun (p : Lean.Lsp.CodeActionParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceInlayHintParams :
FileSource InlayHintParams
Equations

- Lean.Lsp.instFileSourceInlayHintParams = { fileSource := fun (p : Lean.Lsp.InlayHintParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceSignatureHelpParams :
FileSource SignatureHelpParams
Equations

- Lean.Lsp.instFileSourceSignatureHelpParams = { fileSource := fun (p : Lean.Lsp.SignatureHelpParams) => Lean.Lsp.fileSource p.textDocument }

source
instance Lean.Lsp.instFileSourceDocumentColorParams :
FileSource DocumentColorParams
Equations

- Lean.Lsp.instFileSourceDocumentColorParams = { fileSource := fun (p : Lean.Lsp.DocumentColorParams) => Lean.Lsp.fileSource p.textDocument }

source
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.

Equations

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

Instances For

source
instance Lean.Lsp.instFileSourceCompletionItem :
FileSource CompletionItem
Equations

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