The kind of a code action.
Kinds are a hierarchical list of identifiers separated by .
,
e.g. "refactor.extract.function"
.
The set of kinds is open and client needs to announce the kinds it supports to the server during initialization. You can make your own code action kinds, the ones supported by LSP are:
quickfix
refactor
refactor.extract
refactor.inline
refactor.rewrite
source
Source code actions apply to the entire file. Eg fixing all issues or organising imports.source.organizeImports
source.fixAll
Equations
Instances For
- invoked: Lean.Lsp.CodeActionTriggerKind
Code actions were explicitly requested by the user or by an extension.
- automatic: Lean.Lsp.CodeActionTriggerKind
Code actions were requested automatically.
This typically happens when current selection in a file changes, but can also be triggered when file content changes.
Instances For
Contains additional diagnostic information about the context in which a code action is run.
- diagnostics : Array Lean.Lsp.Diagnostic
An array of diagnostics known on the client side overlapping the range provided to the
textDocument/codeAction
request. They are provided so that the server knows which errors are currently presented to the user for the given range. There is no guarantee that these accurately reflect the error state of the resource. The primary parameter to compute code actions is the provided range. - only? : Option (Array Lean.Lsp.CodeActionKind)
Requested kind of actions to return.
Actions not of this kind are filtered out by the client before being shown. So servers can omit computing them.
- triggerKind? : Option Lean.Lsp.CodeActionTriggerKind
The reason why code actions were requested.
Instances For
Parameters for a CodeActionRequest.
- textDocument : Lean.Lsp.TextDocumentIdentifier
- range : Lean.Lsp.Range
- context : Lean.Lsp.CodeActionContext
Instances For
Capabilities of the server for handling code actions.
- codeActionKinds? : Option (Array Lean.Lsp.CodeActionKind)
CodeActionKinds that this server may return.
The list of kinds may be generic, such as
"refactor"
, or the server may list out every specific kind they provide. The server provides support to resolve additional information for a code action.
Instances For
A code action represents a change that can be performed in code, e.g. to fix a problem or to refactor code.
A CodeAction should set either edit
and/or a command
.
If both are supplied, the edit
is applied first, then the command
is executed.
If none are supplied, the client makes a codeAction/resolve
JSON-RPC request to compute the edit.
- title : String
A short, human-readable, title for this code action.
- kind? : Option Lean.Lsp.CodeActionKind
The kind of the code action.
- diagnostics? : Option (Array Lean.Lsp.Diagnostic)
The diagnostics that this code action resolves.
Marks this as a preferred action. Preferred actions are used by the
auto fix
command and can be targeted by keybindings.- disabled? : Option Lean.Lsp.CodeActionDisabled
Marks that the code action cannot currently be applied.
- edit? : Option Lean.Lsp.WorkspaceEdit
The workspace edit this code action performs.
- command? : Option Lean.Lsp.Command
A command this code action executes.
If a code action provides an edit and a command, first the edit is executed and then the command.
A data entry field that is preserved on a code action between a
textDocument/codeAction
and acodeAction/resolve
request. In particular, for Lean-created commands we expectdata
to have auri : DocumentUri
field so thatFileSource
can be implemented.
Instances For
Equations
- Lean.Lsp.instFromJsonCodeAction = { fromJson? := Lean.Lsp.fromJsonCodeAction✝ }
Equations
- Lean.Lsp.instFromJsonResolveSupport = { fromJson? := Lean.Lsp.fromJsonResolveSupport✝ }
Equations
- Lean.Lsp.instToJsonResolveSupport = { toJson := Lean.Lsp.toJsonResolveSupport✝ }
- valueSet : Array Lean.Lsp.CodeActionKind
The code action kind values the client supports. When this property exists the client also guarantees that it will handle values outside its set gracefully and falls back to a default value when unknown.
Instances For
- codeActionKind : Lean.Lsp.CodeActionLiteralSupportValueSet
The code action kind is supported with the following value set.
Instances For
Whether we can register capabilities dynamically.
Whether the code action supports the
isPreferred
property.Whether the code action supports the
disabled
property.Weather code action supports the
data
property which is preserved between atextDocument/codeAction
and acodeAction/resolve
request.Whether the client honors the change annotations in text edits and resource operations returned via the
CodeAction#edit
property by for example presenting the workspace edit in the user interface and asking for confirmation.- codeActionLiteralSupport? : Option Lean.Lsp.CodeActionLiteralSupport
The client supports code action literals as a valid response of the
textDocument/codeAction
request. - resolveSupport? : Option Lean.Lsp.ResolveSupport
Whether the client supports resolving additional code action properties via a separate
codeAction/resolve
request.