@[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

inductive Lean.Lsp.CodeActionTriggerKind : Type

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

  invoked: 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.

  automatic: Lean.Lsp.CodeActionTriggerKind

instance Lean.Lsp.instToJsonCodeActionTriggerKind : Lean.ToJson Lean.Lsp.CodeActionTriggerKind

Equations

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

instance Lean.Lsp.instFromJsonCodeActionTriggerKind : Lean.FromJson Lean.Lsp.CodeActionTriggerKind

Equations

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

structure Lean.Lsp.CodeActionContext : Type

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

  diagnostics : Array Lean.Lsp.Diagnostic

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

  only? : Option (Array Lean.Lsp.CodeActionKind)

• The reason why code actions were requested.

  triggerKind? : Option Lean.Lsp.CodeActionTriggerKind

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

reference

instance Lean.Lsp.instFromJsonCodeActionContext : Lean.FromJson Lean.Lsp.CodeActionContext

Equations

• Lean.Lsp.instFromJsonCodeActionContext = { fromJson? := Lean.Lsp.fromJsonCodeActionContext✝ }

instance Lean.Lsp.instToJsonCodeActionContext : Lean.ToJson Lean.Lsp.CodeActionContext

Equations

• Lean.Lsp.instToJsonCodeActionContext = { toJson := Lean.Lsp.toJsonCodeActionContext✝ }

structure Lean.Lsp.CodeActionParamsextends Lean.Lsp.WorkDoneProgressParams , Lean.Lsp.PartialResultParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier
• range : Lean.Lsp.Range
• context : Lean.Lsp.CodeActionContext

Parameters for a CodeActionRequest.

instance Lean.Lsp.instFromJsonCodeActionParams : Lean.FromJson Lean.Lsp.CodeActionParams

Equations

• Lean.Lsp.instFromJsonCodeActionParams = { fromJson? := Lean.Lsp.fromJsonCodeActionParams✝ }

instance Lean.Lsp.instToJsonCodeActionParams : Lean.ToJson Lean.Lsp.CodeActionParams

Equations

• Lean.Lsp.instToJsonCodeActionParams = { toJson := Lean.Lsp.toJsonCodeActionParams✝ }

structure Lean.Lsp.CodeActionDisabled : Type

• reason : String

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

instance Lean.Lsp.instFromJsonCodeActionDisabled : Lean.FromJson Lean.Lsp.CodeActionDisabled

Equations

• Lean.Lsp.instFromJsonCodeActionDisabled = { fromJson? := Lean.Lsp.fromJsonCodeActionDisabled✝ }

instance Lean.Lsp.instToJsonCodeActionDisabled : Lean.ToJson Lean.Lsp.CodeActionDisabled

Equations

• Lean.Lsp.instToJsonCodeActionDisabled = { toJson := Lean.Lsp.toJsonCodeActionDisabled✝ }

structure Lean.Lsp.CodeActionOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

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

  codeActionKinds? : Option (Array Lean.Lsp.CodeActionKind)

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

  resolveProvider? : Option Bool

Capabilities of the server for handling code actions.

instance Lean.Lsp.instToJsonCodeActionOptions : Lean.ToJson Lean.Lsp.CodeActionOptions

Equations

• Lean.Lsp.instToJsonCodeActionOptions = { toJson := Lean.Lsp.toJsonCodeActionOptions✝ }

instance Lean.Lsp.instFromJsonCodeActionOptions : Lean.FromJson Lean.Lsp.CodeActionOptions

Equations

• Lean.Lsp.instFromJsonCodeActionOptions = { fromJson? := Lean.Lsp.fromJsonCodeActionOptions✝ }

structure Lean.Lsp.CodeActionextends Lean.Lsp.WorkDoneProgressParams , Lean.Lsp.PartialResultParams : Type

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

  title : String

• The kind of the code action.

  kind? : Option Lean.Lsp.CodeActionKind

• The diagnostics that this code action resolves.

  diagnostics? : Option (Array Lean.Lsp.Diagnostic)

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

  isPreferred? : Option Bool

• Marks that the code action cannot currently be applied.

  disabled? : Option Lean.Lsp.CodeActionDisabled

• The workspace edit this code action performs.

  edit? : Option Lean.Lsp.WorkspaceEdit

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

  command? : Option Lean.Lsp.Command

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

  data? : Option Lean.Json

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

instance Lean.Lsp.instToJsonCodeAction : Lean.ToJson Lean.Lsp.CodeAction

Equations

• Lean.Lsp.instToJsonCodeAction = { toJson := Lean.Lsp.toJsonCodeAction✝ }

instance Lean.Lsp.instFromJsonCodeAction : Lean.FromJson Lean.Lsp.CodeAction

Equations

• Lean.Lsp.instFromJsonCodeAction = { fromJson? := Lean.Lsp.fromJsonCodeAction✝ }

structure Lean.Lsp.ResolveSupport : Type

• properties : Array String

instance Lean.Lsp.instFromJsonResolveSupport : Lean.FromJson Lean.Lsp.ResolveSupport

Equations

• Lean.Lsp.instFromJsonResolveSupport = { fromJson? := Lean.Lsp.fromJsonResolveSupport✝ }

instance Lean.Lsp.instToJsonResolveSupport : Lean.ToJson Lean.Lsp.ResolveSupport

Equations

• Lean.Lsp.instToJsonResolveSupport = { toJson := Lean.Lsp.toJsonResolveSupport✝ }

structure Lean.Lsp.CodeActionLiteralSupportValueSet : Type

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

  valueSet : Array Lean.Lsp.CodeActionKind

instance Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet : Lean.FromJson Lean.Lsp.CodeActionLiteralSupportValueSet

Equations

• Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet = { fromJson? := Lean.Lsp.fromJsonCodeActionLiteralSupportValueSet✝ }

instance Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet : Lean.ToJson Lean.Lsp.CodeActionLiteralSupportValueSet

Equations

• Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet = { toJson := Lean.Lsp.toJsonCodeActionLiteralSupportValueSet✝ }

structure Lean.Lsp.CodeActionLiteralSupport : Type

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

  codeActionKind : Lean.Lsp.CodeActionLiteralSupportValueSet

instance Lean.Lsp.instFromJsonCodeActionLiteralSupport : Lean.FromJson Lean.Lsp.CodeActionLiteralSupport

Equations

• Lean.Lsp.instFromJsonCodeActionLiteralSupport = { fromJson? := Lean.Lsp.fromJsonCodeActionLiteralSupport✝ }

instance Lean.Lsp.instToJsonCodeActionLiteralSupport : Lean.ToJson Lean.Lsp.CodeActionLiteralSupport

Equations

• Lean.Lsp.instToJsonCodeActionLiteralSupport = { toJson := Lean.Lsp.toJsonCodeActionLiteralSupport✝ }

structure Lean.Lsp.CodeActionClientCapabilities : Type

• Whether we can register capabilities dynamically.

  dynamicRegistration? : Option Bool

• Whether the code action supports the isPreferred property.

  isPreferredSupport? : Option Bool

• Whether the code action supports the disabled property.

  disabledSupport? : Option Bool

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

  dataSupport? : 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.

  honorsChangeAnnotations? : Option Bool

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

  codeActionLiteralSupport? : Option Lean.Lsp.CodeActionLiteralSupport

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

  resolveSupport? : Option Lean.Lsp.ResolveSupport

Reference

instance Lean.Lsp.instFromJsonCodeActionClientCapabilities : Lean.FromJson Lean.Lsp.CodeActionClientCapabilities

Equations

• Lean.Lsp.instFromJsonCodeActionClientCapabilities = { fromJson? := Lean.Lsp.fromJsonCodeActionClientCapabilities✝ }

instance Lean.Lsp.instToJsonCodeActionClientCapabilities : Lean.ToJson Lean.Lsp.CodeActionClientCapabilities

Equations

• Lean.Lsp.instToJsonCodeActionClientCapabilities = { toJson := Lean.Lsp.toJsonCodeActionClientCapabilities✝ }