# Initial setup for code actions #

This declares a code action provider that calls all `@[hole_code_action]` definitions on each occurrence of a hole (`_`, `?_` or `sorry`).

(This is in a separate file from `Std.CodeAction.Hole.Attr` so that the server does not attempt to use this code action provider when browsing the `Std.CodeAction.Hole.Attr` file itself.)

source
def Lean.CodeAction.holeCodeActionProvider :
Server.CodeActionProvider

A code action which calls all `@[hole_code_action]` code actions on each hole (`?_`, `_`, or `sorry`).

Instances For

source
inductive Lean.CodeAction.FindTacticResult :
Type

The return value of `findTactic?`. This is the syntax for which code actions will be triggered.

- tactic : Syntax.Stack → FindTacticResult

  The nearest enclosing tactic is a tactic, with the given syntax stack.

- tacticSeq (preferred : Bool) (insertIdx : Nat) : Syntax.Stack → FindTacticResult

  The cursor is between tactics, and the nearest enclosing range is a tactic sequence. Code actions will insert tactics at index `insertIdx` into the syntax (which is a nullNode of `tactic;*` inside a `tacticSeqBracketed` or `tacticSeq1Indented`).

Instances For

source
def Lean.CodeAction.findTactic? (preferred : String.Pos.Raw → Bool) (range : String.Range) (root : Syntax) :
Option FindTacticResult

Find the syntax on which to trigger tactic code actions. This is a pure syntax pass, without regard to elaboration information.

- `preferred : String.Pos → Bool`: used to select "preferred `tacticSeq`s" based on the cursor column, when the cursor selection would otherwise be ambiguous. For example, in:

      · foo
        · bar
          baz
        |

  where the cursor is at the `|`, we select the `tacticSeq` starting with `foo`, while if the cursor was indented to align with `baz` then we would select the `bar; baz` sequence instead.

- `range`: the cursor selection. We do not do much with range selections; if a range selection covers more than one tactic then we abort.

- `root`: the root syntax to process

The return value is either a selected tactic, or a selected point in a tactic sequence.

Equations

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

Instances For

source
partial def Lean.CodeAction.findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range) (ctx? : Option Elab.ContextInfo) (t : Elab.InfoTree) (f : Elab.ContextInfo → Elab.Info → Bool) (canonicalOnly : Bool := false) :
Option (Elab.ContextInfo × Elab.InfoTree)

Returns the info tree corresponding to a syntax, using `kind` and `range` for identification. (This is not foolproof, but it is a fairly accurate proxy for `Syntax` equality and a lot cheaper than deep comparison.)

source
def Lean.CodeAction.cmdCodeActionProvider :
Server.CodeActionProvider

A code action which calls all `@[command_code_action]` code actions on each command.

Equations

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

Instances For