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 @[tactic_code_action] collects code actions which will be called on each occurrence of a tactic.

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

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

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

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

Equations

• Lean.CodeAction.mkHoleCodeAction n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (Lean.CodeAction.mkHoleCodeAction.unsafe_impl_1 n env opts))

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

An extension which collects all the hole code actions.

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

def Lean.CodeAction.mkCommandCodeAction (n : Lake.Name) : Lean.ImportM Lean.CodeAction.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.

structure Lean.CodeAction.CommandCodeActionEntry : Type

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

• declName : Lake.Name

  The declaration to tag

• cmdKinds : Array Lake.Name

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

instance Lean.CodeAction.instInhabitedCommandCodeActionEntry : Inhabited Lean.CodeAction.CommandCodeActionEntry

Equations

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

structure Lean.CodeAction.CommandCodeActions : Type

The state of the command code actions extension.

• onAnyCmd : Array Lean.CodeAction.CommandCodeAction

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

• onCmd : Lake.NameMap (Array Lean.CodeAction.CommandCodeAction)

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

instance Lean.CodeAction.instInhabitedCommandCodeActions : Inhabited Lean.CodeAction.CommandCodeActions

Equations

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

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

Insert a command code action entry into the CommandCodeActions structure.

Equations

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

opaque Lean.CodeAction.builtinCmdCodeActions : IO.Ref Lean.CodeAction.CommandCodeActions

def Lean.CodeAction.insertBuiltin (args : Array Lake.Name) (proc : Lean.CodeAction.CommandCodeAction) : IO Unit

Equations

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

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

An extension which collects all the command code actions.