structure Lean.Server.LazyCodeAction : Type

A code action optionally supporting a lazy code action computation that is only run when the user clicks on the code action in the editor.

If you want to use the lazy feature, make sure that the edit? field on the eager code action result is none.

• eager : Lean.Lsp.CodeAction

  This is the initial code action that is sent to the server, to implement

• lazy? : Option (IO Lean.Lsp.CodeAction)

structure Lean.Server.CodeActionResolveData : Type

Passed as the data? field of Lsp.CodeAction to recover the context of the code action.

• params : Lean.Lsp.CodeActionParams
• providerName : Lake.Name

  Name of CodeActionProvider that produced this request.

• providerResultIndex : Nat

  Index in the list of code action that the given provider generated.

instance Lean.Server.instToJsonCodeActionResolveData : Lean.ToJson Lean.Server.CodeActionResolveData

Equations

• Lean.Server.instToJsonCodeActionResolveData = { toJson := Lean.Server.toJsonCodeActionResolveData✝ }

instance Lean.Server.instFromJsonCodeActionResolveData : Lean.FromJson Lean.Server.CodeActionResolveData

Equations

• Lean.Server.instFromJsonCodeActionResolveData = { fromJson? := Lean.Server.fromJsonCodeActionResolveData✝ }

def Lean.Server.CodeAction.getFileSource! (ca : Lean.Lsp.CodeAction) : Lean.Lsp.DocumentUri

Equations

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

instance Lean.Server.instFileSourceCodeAction : Lean.Lsp.FileSource Lean.Lsp.CodeAction

Equations

• Lean.Server.instFileSourceCodeAction = { fileSource := fun (x : Lean.Lsp.CodeAction) => Lean.Server.CodeAction.getFileSource! x }

instance Lean.Server.instCoeCodeActionLazyCodeAction : Coe Lean.Lsp.CodeAction Lean.Server.LazyCodeAction

Equations

• Lean.Server.instCoeCodeActionLazyCodeAction = { coe := fun (c : Lean.Lsp.CodeAction) => { eager := c, lazy? := none } }

def Lean.Server.CodeActionProvider : Type

A code action provider is a function for providing LSP code actions for an editor. You can register them with the @[code_action_provider] attribute.

This is a low-level interface for making LSP code actions. This interface can be used to implement the following applications:

• refactoring code: adding underscores to unused variables,
• suggesting imports
• document-level refactoring: removing unused imports, sorting imports, formatting.
• Helper suggestions for working with type holes (_)
• Helper suggestions for tactics.

When implementing your own CodeActionProvider, we assume that no long-running computations are allowed. If you need to create a code-action with a long-running computation, you can use the lazy? field on LazyCodeAction to perform the computation after the user has clicked on the code action in their editor.

Equations

• Lean.Server.CodeActionProvider = (Lean.Lsp.CodeActionParams → Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM (Array Lean.Server.LazyCodeAction))

def Lean.Server.addBuiltinCodeActionProvider (decl : Lake.Name) (provider : Lean.Server.CodeActionProvider) : IO Unit

Equations

• Lean.Server.addBuiltinCodeActionProvider decl provider = ST.Ref.modify Lean.Server.builtinCodeActionProviders fun (x : Lake.NameMap Lean.Server.CodeActionProvider) => x.insert decl provider

opaque Lean.Server.codeActionProviderExt : Lean.SimplePersistentEnvExtension Lake.Name Lean.NameSet

def Lean.Server.handleCodeAction (params : Lean.Lsp.CodeActionParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.CodeAction))

Handles a textDocument/codeAction request.

This is implemented by calling all of the registered CodeActionProvider functions.

reference.

Equations

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

def Lean.Server.handleCodeActionResolve (param : Lean.Lsp.CodeAction) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.CodeAction)

Handler for "codeAction/resolve".

reference

Equations

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