# Initial setup for code action attributes #

- Attribute `@[hole_code_action]` collects code actions which will be called on each occurrence of a hole (`_`, `?_` or `sorry`).

- Attribute `@[command_code_action]` collects code actions which will be called on each occurrence of a command.

source
@[reducible, inline]
abbrev Lean.CodeAction.HoleCodeAction :
Type

A hole code action extension.

Equations

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

Instances For

source
def Lean.CodeAction.mkHoleCodeAction (n : Name) :
ImportM HoleCodeAction

Read a hole code action from a declaration of the right type.

Equations

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

Instances For

source
opaque Lean.CodeAction.holeCodeActionExt :
PersistentEnvExtension Name (Name × HoleCodeAction) (Array Name × Array HoleCodeAction)

An extension which collects all the hole code actions.

source
@[reducible, inline]
abbrev Lean.CodeAction.CommandCodeAction :
Type

A command code action extension.

Equations

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

Instances For

source
def Lean.CodeAction.mkCommandCodeAction (n : Name) :
ImportM CommandCodeAction

Read a command code action from a declaration of the right type.

Equations

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

Instances For

source
structure Lean.CodeAction.CommandCodeActionEntry :
Type

An entry in the command code actions extension, containing the attribute arguments.

- declName : Name

  The declaration to tag

- cmdKinds : Array Name

  The command kinds that this extension supports. If empty it is called on all command kinds.

Instances For

source
instance Lean.CodeAction.instInhabitedCommandCodeActionEntry :
Inhabited CommandCodeActionEntry
Equations

- Lean.CodeAction.instInhabitedCommandCodeActionEntry = { default := Lean.CodeAction.instInhabitedCommandCodeActionEntry.default }

source
def Lean.CodeAction.instInhabitedCommandCodeActionEntry.default :
CommandCodeActionEntry
Equations

- Lean.CodeAction.instInhabitedCommandCodeActionEntry.default = { declName := default, cmdKinds := default }

Instances For

source
structure Lean.CodeAction.CommandCodeActions :
Type

The state of the command code actions extension.

- onAnyCmd : Array CommandCodeAction

  The list of command code actions to apply on any command.

- onCmd : NameMap (Array CommandCodeAction)

  The list of command code actions to apply when a particular command kind is highlighted.

Instances For

source
instance Lean.CodeAction.instInhabitedCommandCodeActions :
Inhabited CommandCodeActions
Equations

- Lean.CodeAction.instInhabitedCommandCodeActions = { default := Lean.CodeAction.instInhabitedCommandCodeActions.default }

source
def Lean.CodeAction.instInhabitedCommandCodeActions.default :
CommandCodeActions
Equations

- Lean.CodeAction.instInhabitedCommandCodeActions.default = { onAnyCmd := default, onCmd := default }

Instances For

source
def Lean.CodeAction.CommandCodeActions.insert (self : CommandCodeActions) (tacticKinds : Array Name) (action : CommandCodeAction) :
CommandCodeActions

Insert a command code action entry into the `CommandCodeActions` structure.

Equations

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

Instances For

source
opaque Lean.CodeAction.builtinCmdCodeActions :
IO.Ref CommandCodeActions
source
def Lean.CodeAction.insertBuiltin (args : Array Name) (proc : CommandCodeAction) :
IO Unit
Equations

- Lean.CodeAction.insertBuiltin args proc = ST.Ref.modify Lean.CodeAction.builtinCmdCodeActions fun (self : Lean.CodeAction.CommandCodeActions) => self.insert args proc

Instances For

source
opaque Lean.CodeAction.cmdCodeActionExt :
PersistentEnvExtension CommandCodeActionEntry (CommandCodeActionEntry × CommandCodeAction) (Array CommandCodeActionEntry × CommandCodeActions)

An extension which collects all the command code actions.