Documentation

Lean.Server.CodeActions.Provider

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

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

Instances For

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

    Instances For

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

      • preferred : String.PosBool: 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.
      Instances For

        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.
        Instances For

          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
          Instances For

            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.

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

            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