From ad4b822734adfd7800194eb574b31fe540923302 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 8 May 2023 15:14:51 -0400
Subject: [PATCH] fix: use snake case for `@[code_action_provider]`

---
 src/Lean/Server/CodeActions.lean       | 4 ++--
 tests/lean/interactive/codeaction.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Server/CodeActions.lean b/src/Lean/Server/CodeActions.lean
index b95db3e57e..7424d5b25b 100644
--- a/src/Lean/Server/CodeActions.lean
+++ b/src/Lean/Server/CodeActions.lean
@@ -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)
diff --git a/tests/lean/interactive/codeaction.lean b/tests/lean/interactive/codeaction.lean
index 60df5adb33..1ae5a6aa4e 100644
--- a/tests/lean/interactive/codeaction.lean
+++ b/tests/lean/interactive/codeaction.lean
@@ -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 := {