source
@[reducible, inline]
abbrev Lean.Lsp.CodeActionKind :
Type

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

- Lean.Lsp.CodeActionKind = String

Instances For

source
inductive Lean.Lsp.CodeActionTriggerKind :
Type

- invoked : CodeActionTriggerKind

  Code actions were explicitly requested by the user or by an extension.

- automatic : 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

source
instance Lean.Lsp.instToJsonCodeActionTriggerKind :
ToJson CodeActionTriggerKind
Equations

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

source
instance Lean.Lsp.instFromJsonCodeActionTriggerKind :
FromJson CodeActionTriggerKind
Equations

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

source
structure Lean.Lsp.CodeActionContext :
Type

Contains additional diagnostic information about the context in which a code action is run.

reference

- diagnostics : Array 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 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 CodeActionTriggerKind

  The reason why code actions were requested.

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionContext :
FromJson CodeActionContext
Equations

- Lean.Lsp.instFromJsonCodeActionContext = { fromJson? := Lean.Lsp.instFromJsonCodeActionContext.fromJson }

source
def Lean.Lsp.instFromJsonCodeActionContext.fromJson :
Json → Except String CodeActionContext
Equations

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

Instances For

source
def Lean.Lsp.instToJsonCodeActionContext.toJson :
CodeActionContext → Json
Equations

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

Instances For

source
instance Lean.Lsp.instToJsonCodeActionContext :
ToJson CodeActionContext
Equations

- Lean.Lsp.instToJsonCodeActionContext = { toJson := Lean.Lsp.instToJsonCodeActionContext.toJson }

source
structure Lean.Lsp.CodeActionParams extends Lean.Lsp.WorkDoneProgressParams, Lean.Lsp.PartialResultParams :
Type

Parameters for a CodeActionRequest.

- workDoneToken? : Option ProgressToken
- partialResultToken? : Option ProgressToken
- textDocument : TextDocumentIdentifier
- range : Range
- context : CodeActionContext

Instances For

source
def Lean.Lsp.instFromJsonCodeActionParams.fromJson :
Json → Except String CodeActionParams
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionParams :
FromJson CodeActionParams
Equations

- Lean.Lsp.instFromJsonCodeActionParams = { fromJson? := Lean.Lsp.instFromJsonCodeActionParams.fromJson }

source
instance Lean.Lsp.instToJsonCodeActionParams :
ToJson CodeActionParams
Equations

- Lean.Lsp.instToJsonCodeActionParams = { toJson := Lean.Lsp.instToJsonCodeActionParams.toJson }

source
def Lean.Lsp.instToJsonCodeActionParams.toJson :
CodeActionParams → Json
Equations

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

Instances For

source
structure Lean.Lsp.CodeActionDisabled :
Type

If the code action is disabled, this type gives the reason why.

- reason : String

Instances For

source
def Lean.Lsp.instFromJsonCodeActionDisabled.fromJson :
Json → Except String CodeActionDisabled
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionDisabled :
FromJson CodeActionDisabled
Equations

- Lean.Lsp.instFromJsonCodeActionDisabled = { fromJson? := Lean.Lsp.instFromJsonCodeActionDisabled.fromJson }

source
def Lean.Lsp.instToJsonCodeActionDisabled.toJson :
CodeActionDisabled → Json
Equations

- Lean.Lsp.instToJsonCodeActionDisabled.toJson x✝ = Lean.Json.mkObj [[("reason", Lean.toJson x✝.reason)]].flatten

Instances For

source
instance Lean.Lsp.instToJsonCodeActionDisabled :
ToJson CodeActionDisabled
Equations

- Lean.Lsp.instToJsonCodeActionDisabled = { toJson := Lean.Lsp.instToJsonCodeActionDisabled.toJson }

source
structure Lean.Lsp.CodeActionOptions extends Lean.Lsp.WorkDoneProgressOptions :
Type

Capabilities of the server for handling code actions.

- workDoneProgress : Bool
- codeActionKinds? : Option (Array 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.

- resolveProvider? : Option Bool

  The server provides support to resolve additional information for a code action.

Instances For

source
instance Lean.Lsp.instToJsonCodeActionOptions :
ToJson CodeActionOptions
Equations

- Lean.Lsp.instToJsonCodeActionOptions = { toJson := Lean.Lsp.instToJsonCodeActionOptions.toJson }

source
def Lean.Lsp.instToJsonCodeActionOptions.toJson :
CodeActionOptions → Json
Equations

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

Instances For

source
def Lean.Lsp.instFromJsonCodeActionOptions.fromJson :
Json → Except String CodeActionOptions
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionOptions :
FromJson CodeActionOptions
Equations

- Lean.Lsp.instFromJsonCodeActionOptions = { fromJson? := Lean.Lsp.instFromJsonCodeActionOptions.fromJson }

source
structure Lean.Lsp.CodeAction extends Lean.Lsp.WorkDoneProgressParams, Lean.Lsp.PartialResultParams :
Type

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.

reference

- workDoneToken? : Option ProgressToken
- partialResultToken? : Option ProgressToken
- title : String

  A short, human-readable, title for this code action.

- kind? : Option CodeActionKind

  The kind of the code action.

- diagnostics? : Option (Array Diagnostic)

  The diagnostics that this code action resolves.

- isPreferred? : Option Bool

  Marks this as a preferred action. Preferred actions are used by the `auto fix` command and can be targeted by keybindings.

- disabled? : Option CodeActionDisabled

  Marks that the code action cannot currently be applied.

- edit? : Option WorkspaceEdit

  The workspace edit this code action performs.

- command? : Option 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.

- data? : Option Json

  A data entry field that is preserved on a code action between a `textDocument/codeAction` and a `codeAction/resolve` request. In particular, for Lean-created commands we expect `data` to have a `uri : DocumentUri` field so that `FileSource` can be implemented.

Instances For

source
def Lean.Lsp.instToJsonCodeAction.toJson :
CodeAction → Json
Equations

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

Instances For

source
instance Lean.Lsp.instToJsonCodeAction :
ToJson CodeAction
Equations

- Lean.Lsp.instToJsonCodeAction = { toJson := Lean.Lsp.instToJsonCodeAction.toJson }

source
instance Lean.Lsp.instFromJsonCodeAction :
FromJson CodeAction
Equations

- Lean.Lsp.instFromJsonCodeAction = { fromJson? := Lean.Lsp.instFromJsonCodeAction.fromJson }

source
def Lean.Lsp.instFromJsonCodeAction.fromJson :
Json → Except String CodeAction
Equations

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

Instances For

source
structure Lean.Lsp.CodeActionLiteralSupportValueSet :
Type

- valueSet : Array 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

source
def Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet.fromJson :
Json → Except String CodeActionLiteralSupportValueSet
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet :
FromJson CodeActionLiteralSupportValueSet
Equations

- Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet = { fromJson? := Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet.fromJson }

source
def Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet.toJson :
CodeActionLiteralSupportValueSet → Json
Equations

- Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet.toJson x✝ = Lean.Json.mkObj [[("valueSet", Lean.toJson x✝.valueSet)]].flatten

Instances For

source
instance Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet :
ToJson CodeActionLiteralSupportValueSet
Equations

- Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet = { toJson := Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet.toJson }

source
structure Lean.Lsp.CodeActionLiteralSupport :
Type

- codeActionKind : CodeActionLiteralSupportValueSet

  The code action kind is supported with the following value set.

Instances For

source
def Lean.Lsp.instFromJsonCodeActionLiteralSupport.fromJson :
Json → Except String CodeActionLiteralSupport
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionLiteralSupport :
FromJson CodeActionLiteralSupport
Equations

- Lean.Lsp.instFromJsonCodeActionLiteralSupport = { fromJson? := Lean.Lsp.instFromJsonCodeActionLiteralSupport.fromJson }

source
instance Lean.Lsp.instToJsonCodeActionLiteralSupport :
ToJson CodeActionLiteralSupport
Equations

- Lean.Lsp.instToJsonCodeActionLiteralSupport = { toJson := Lean.Lsp.instToJsonCodeActionLiteralSupport.toJson }

source
def Lean.Lsp.instToJsonCodeActionLiteralSupport.toJson :
CodeActionLiteralSupport → Json
Equations

- Lean.Lsp.instToJsonCodeActionLiteralSupport.toJson x✝ = Lean.Json.mkObj [[("codeActionKind", Lean.toJson x✝.codeActionKind)]].flatten

Instances For

source
structure Lean.Lsp.CodeActionClientCapabilities :
Type

Reference

- dynamicRegistration? : Option Bool

  Whether we can register capabilities dynamically.

- isPreferredSupport? : Option Bool

  Whether the code action supports the `isPreferred` property.

- disabledSupport? : Option Bool

  Whether the code action supports the `disabled` property.

- dataSupport? : Option Bool

  Weather code action supports the `data` property which is preserved between a `textDocument/codeAction` and a `codeAction/resolve` request.

- honorsChangeAnnotations? : Option Bool

  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 CodeActionLiteralSupport

  The client supports code action literals as a valid response of the `textDocument/codeAction` request.

- resolveSupport? : Option ResolveSupport

  Whether the client supports resolving additional code action properties via a separate `codeAction/resolve` request.

Instances For

source
def Lean.Lsp.instFromJsonCodeActionClientCapabilities.fromJson :
Json → Except String CodeActionClientCapabilities
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonCodeActionClientCapabilities :
FromJson CodeActionClientCapabilities
Equations

- Lean.Lsp.instFromJsonCodeActionClientCapabilities = { fromJson? := Lean.Lsp.instFromJsonCodeActionClientCapabilities.fromJson }

source
def Lean.Lsp.instToJsonCodeActionClientCapabilities.toJson :
CodeActionClientCapabilities → Json
Equations

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

Instances For

source
instance Lean.Lsp.instToJsonCodeActionClientCapabilities :
ToJson CodeActionClientCapabilities
Equations

- Lean.Lsp.instToJsonCodeActionClientCapabilities = { toJson := Lean.Lsp.instToJsonCodeActionClientCapabilities.toJson }