- uri (uri : DocumentUri) : FileIdent
- mod (mod : Name) : FileIdent
Instances For
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Lsp.instFileSourceLocation = { fileSource := fun (l : Lean.Lsp.Location) => Lean.Lsp.FileIdent.uri l.uri }
Equations
- Lean.Lsp.instFileSourceTextDocumentIdentifier = { fileSource := fun (i : Lean.Lsp.TextDocumentIdentifier) => Lean.Lsp.FileIdent.uri i.uri }
Equations
- Lean.Lsp.instFileSourceVersionedTextDocumentIdentifier = { fileSource := fun (i : Lean.Lsp.VersionedTextDocumentIdentifier) => Lean.Lsp.FileIdent.uri i.uri }
Equations
- Lean.Lsp.instFileSourceTextDocumentEdit = { fileSource := fun (e : Lean.Lsp.TextDocumentEdit) => Lean.Lsp.fileSource e.textDocument }
Equations
- Lean.Lsp.instFileSourceTextDocumentItem = { fileSource := fun (i : Lean.Lsp.TextDocumentItem) => Lean.Lsp.FileIdent.uri i.uri }
Equations
- Lean.Lsp.instFileSourceTextDocumentPositionParams = { fileSource := fun (p : Lean.Lsp.TextDocumentPositionParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidOpenTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidOpenTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidChangeTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidChangeTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidSaveTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidSaveTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceDidCloseTextDocumentParams = { fileSource := fun (p : Lean.Lsp.DidCloseTextDocumentParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceCompletionParams = { fileSource := fun (h : Lean.Lsp.CompletionParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceHoverParams = { fileSource := fun (h : Lean.Lsp.HoverParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceDeclarationParams = { fileSource := fun (h : Lean.Lsp.DeclarationParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceDefinitionParams = { fileSource := fun (h : Lean.Lsp.DefinitionParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceTypeDefinitionParams = { fileSource := fun (h : Lean.Lsp.TypeDefinitionParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceReferenceParams = { fileSource := fun (h : Lean.Lsp.ReferenceParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceWaitForDiagnosticsParams = { fileSource := fun (p : Lean.Lsp.WaitForDiagnosticsParams) => Lean.Lsp.FileIdent.uri p.uri }
Equations
- Lean.Lsp.instFileSourceDocumentHighlightParams = { fileSource := fun (h : Lean.Lsp.DocumentHighlightParams) => Lean.Lsp.fileSource h.toTextDocumentPositionParams }
Equations
- Lean.Lsp.instFileSourceDocumentSymbolParams = { fileSource := fun (p : Lean.Lsp.DocumentSymbolParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceSemanticTokensParams = { fileSource := fun (p : Lean.Lsp.SemanticTokensParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceSemanticTokensRangeParams = { fileSource := fun (p : Lean.Lsp.SemanticTokensRangeParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceFoldingRangeParams = { fileSource := fun (p : Lean.Lsp.FoldingRangeParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourcePlainGoalParams = { fileSource := fun (p : Lean.Lsp.PlainGoalParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourcePlainTermGoalParams = { fileSource := fun (p : Lean.Lsp.PlainTermGoalParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceRpcConnectParams = { fileSource := fun (p : Lean.Lsp.RpcConnectParams) => Lean.Lsp.FileIdent.uri p.uri }
Equations
- Lean.Lsp.instFileSourceRpcCallParams = { fileSource := fun (p : Lean.Lsp.RpcCallParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceRpcReleaseParams = { fileSource := fun (p : Lean.Lsp.RpcReleaseParams) => Lean.Lsp.FileIdent.uri p.uri }
Equations
- Lean.Lsp.instFileSourceRpcKeepAliveParams = { fileSource := fun (p : Lean.Lsp.RpcKeepAliveParams) => Lean.Lsp.FileIdent.uri p.uri }
Equations
- Lean.Lsp.instFileSourceCodeActionParams = { fileSource := fun (p : Lean.Lsp.CodeActionParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceInlayHintParams = { fileSource := fun (p : Lean.Lsp.InlayHintParams) => Lean.Lsp.fileSource p.textDocument }
Equations
- Lean.Lsp.instFileSourceSignatureHelpParams = { fileSource := fun (p : Lean.Lsp.SignatureHelpParams) => Lean.Lsp.fileSource p.textDocument }
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.