fix: use snake case for @[code_action_provider]

This commit is contained in:
Mario Carneiro 2023-05-08 15:14:51 -04:00 committed by Sebastian Ullrich
parent 445fd417be
commit ad4b822734
2 changed files with 3 additions and 3 deletions

View file

@ -51,7 +51,7 @@ instance : Coe CodeAction LazyCodeAction where
coe c := { eager := c }
/-- A code action provider is a function for providing LSP code actions for an editor.
You can register them with the `@[codeActionProvider]` attribute.
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:
@ -75,7 +75,7 @@ builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name Nam
}
builtin_initialize registerBuiltinAttribute {
name := `codeActionProvider
name := `code_action_provider
descr := "Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
add := fun src _stx _kind => do
modifyEnv (codeActionProviderExt.addEntry · src)

View file

@ -2,7 +2,7 @@ import Lean
open Lean Server Lsp
@[codeActionProvider]
@[code_action_provider]
def helloProvider : CodeActionProvider := fun params _snap => do
let td := params.textDocument
let edit : TextEdit := {