Initial setup for code action attributes #
Attribute
@[hole_code_action]
collects code actions which will be called on each occurrence of a hole (_
,?_
orsorry
).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.
A hole code action extension.
Equations
Instances For
Read a hole code action from a declaration of the right type.
Equations
Instances For
An extension which collects all the hole code actions.
A command code action extension.
Equations
Instances For
Read a command code action from a declaration of the right type.
Equations
Instances For
An entry in the command code actions extension, containing the attribute arguments.
- declName : Name
The declaration to tag
The command kinds that this extension supports. If empty it is called on all command kinds.
Instances For
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
Equations
Insert a command code action entry into the CommandCodeActions
structure.
Equations
Instances For
Equations
Instances For
An extension which collects all the command code actions.