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

inductive Std.CodeAction.FindTacticResult : Type

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

• tactic: Lean.Syntax.Stack → Std.CodeAction.FindTacticResult

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

• tacticSeq: Bool → Nat → Lean.Syntax.Stack → Std.CodeAction.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).

def Std.CodeAction.findTactic? (preferred : String.Pos → Bool) (range : String.Range) (root : Lean.Syntax) : Option Std.CodeAction.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 tacticSeqs" 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.

def Std.CodeAction.findTactic?.visit (range : String.Range) (stx : Lean.Syntax) (prev? : optParam (Option String.Pos) none) : Option Bool

Returns none if we should not visit this syntax at all, and some false if we only want to visit it in "extended" mode (where we include trailing characters).

Equations

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

def Std.CodeAction.findTactic?.merge (r₁ : Option Std.CodeAction.FindTacticResult) (r₂ : Std.CodeAction.FindTacticResult) : Std.CodeAction.FindTacticResult

Merges the results of two FindTacticResults. This just prefers the second (inner) one, unless the inner tactic is a dispreferred tactic sequence and the outer one is preferred. This is used to implement whitespace-sensitive selection of tactic sequences.

Equations

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

partial def Std.CodeAction.findTactic?.go (preferred : String.Pos → Bool) (range : String.Range) (stack : Lean.Syntax.Stack) (stx : Lean.Syntax) (prev? : optParam (Option String.Pos) none) : Option (Option Std.CodeAction.FindTacticResult)

Main recursion for findTactic?. This takes a stack context and a root syntax stx, and returns the best FindTacticResult it can find. It returns none (abort) if two or more results are found, and some none (none yet) if no results are found.

partial def Std.CodeAction.findInfoTree? (kind : Lean.SyntaxNodeKind) (tgtRange : String.Range) (ctx? : Option Lean.Elab.ContextInfo) (t : Lean.Elab.InfoTree) (f : Lean.Elab.ContextInfo → Lean.Elab.Info → Bool) (canonicalOnly : optParam Bool false) : Option (Lean.Elab.ContextInfo × Lean.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.)

def Std.CodeAction.tacticCodeActionProvider : Lean.Server.CodeActionProvider

A code action which calls @[tactic_code_action] code actions.

Equations

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