diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index bcc3393e34..7d64e48500 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -532,3 +532,65 @@ except that it doesn't print an empty diagnostic.
 (This is effectively a synonym for `run_elab`.)
 -/
 syntax (name := runMeta) "run_meta " doSeq : command
+
+/-- Element that can be part of a `#guard_msgs` specification. -/
+syntax guardMsgsSpecElt := &"drop"? (&"info" <|> &"warning" <|> &"error" <|> &"all")
+
+/-- Specification for `#guard_msgs` command. -/
+syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
+
+/--
+`#guard_msgs` captures the messages generated by another command and checks that they
+match the contents of the docstring attached to the `#guard_msgs` command.
+
+Basic example:
+```lean
+/--
+error: unknown identifier 'x'
+-/
+#guard_msgs in
+example : α := x
+```
+This checks that there is such an error and then consumes the message entirely.
+
+By default, the command intercepts all messages, but there is a way to specify which types
+of messages to consider. For example, we can select only warnings:
+```lean
+/--
+warning: declaration uses 'sorry'
+-/
+#guard_msgs(warning) in
+example : α := sorry
+```
+or only errors
+```lean
+#guard_msgs(error) in
+example : α := sorry
+```
+In this last example, since the message is not intercepted there is a warning on `sorry`.
+We can drop the warning completely with
+```lean
+#guard_msgs(error, drop warning) in
+example : α := sorry
+```
+
+Syntax description:
+```
+#guard_msgs (drop? info|warning|error|all,*)? in cmd
+```
+
+If there is no specification, `#guard_msgs` intercepts all messages.
+Otherwise, if there is one, the specification is considered in left-to-right order, and the first
+that applies chooses the outcome of the message:
+- `info`, `warning`, `error`: intercept a message with the given severity level.
+- `all`: intercept any message (so `#guard_msgs in cmd` and `#guard_msgs (all) in cmd`
+  are equivalent).
+- `drop info`, `drop warning`, `drop error`: intercept a message with the given severity
+  level and then drop it. These messages are not checked.
+- `drop all`: intercept a message and drop it.
+
+For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and then drop
+everything else.
+-/
+syntax (name := guardMsgsCmd)
+  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index 460aca489c..e6b214a3ba 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -86,6 +86,10 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)
 
+/-- Gets the LSP range from a `String.Range`. -/
+def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
+  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
+
 end FileMap
 end Lean
 
diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index eeca035b8f..7bb4e1ac76 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -47,3 +47,4 @@ import Lean.Elab.Eval
 import Lean.Elab.Calc
 import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
+import Lean.Elab.GuardMsgs
diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
new file mode 100644
index 0000000000..ea4d3aa17d
--- /dev/null
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean.Server.CodeActions.Attr
+
+/-! `#guard_msgs` command for testing commands
+
+This module defines a command to test that another command produces the expected messages.
+See the docstring on the `#guard_msgs` command.
+-/
+
+open Lean Parser.Tactic Elab Command
+
+namespace Lean.Elab.Tactic.GuardMsgs
+
+/-- Gives a string representation of a message without source position information.
+Ensures the message ends with a '\n'. -/
+private def messageToStringWithoutPos (msg : Message) : IO String := do
+  let mut str ← msg.data.toString
+  unless msg.caption == "" do
+    str := msg.caption ++ ":\n" ++ str
+  if !("\n".isPrefixOf str) then str := " " ++ str
+  match msg.severity with
+  | MessageSeverity.information => str := "info:" ++ str
+  | MessageSeverity.warning     => str := "warning:" ++ str
+  | MessageSeverity.error       => str := "error:" ++ str
+  if str.isEmpty || str.back != '\n' then
+    str := str ++ "\n"
+  return str
+
+/-- The decision made by a specification for a message. -/
+inductive SpecResult
+  /-- Capture the message and check it matches the docstring. -/
+  | check
+  /-- Drop the message and delete it. -/
+  | drop
+  /-- Do not capture the message. -/
+  | passthrough
+
+/-- Parses a `guardMsgsSpec`.
+- No specification: check everything.
+- With a specification: interpret the spec, and if nothing applies pass it through. -/
+def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
+    CommandElabM (Message → SpecResult) := do
+  if let some spec := spec? then
+    match spec with
+    | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => do
+      let mut p : Message → SpecResult := fun _ => .passthrough
+      let pushP (s : MessageSeverity) (drop : Bool) (p : Message → SpecResult)
+          (msg : Message) : SpecResult :=
+        if msg.severity == s then if drop then .drop else .check
+        else p msg
+      for elt in elts.reverse do
+        match elt with
+        | `(guardMsgsSpecElt| $[drop%$drop?]? info)    => p := pushP .information drop?.isSome p
+        | `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p := pushP .warning drop?.isSome p
+        | `(guardMsgsSpecElt| $[drop%$drop?]? error)   => p := pushP .error drop?.isSome p
+        | `(guardMsgsSpecElt| $[drop%$drop?]? all) =>
+          p := fun _ => if drop?.isSome then .drop else .check
+        | _ => throwErrorAt elt "Invalid #guard_msgs specification element"
+      return p
+    | _ => throwErrorAt spec "Invalid #guard_msgs specification"
+  else
+    return fun _ => .check
+
+/-- An info tree node corresponding to a failed `#guard_msgs` invocation,
+used for code action support. -/
+structure GuardMsgFailure where
+  /-- The result of the nested command -/
+  res : String
+deriving TypeName
+
+@[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
+  | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
+    let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
+    let specFn ← parseGuardMsgsSpec spec?
+    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+    elabCommandTopLevel cmd
+    let msgs := (← get).messages
+    let mut toCheck : MessageLog := .empty
+    let mut toPassthrough : MessageLog := .empty
+    for msg in msgs.toList do
+      match specFn msg with
+      | .check       => toCheck := toCheck.add msg
+      | .drop        => pure ()
+      | .passthrough => toPassthrough := toPassthrough.add msg
+    let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
+    -- We do some whitespace normalization here to allow users to break long lines.
+    if expected.replace "\n" " " == res.replace "\n" " " then
+      -- Passed. Only put toPassthrough messages back on the message log
+      modify fun st => { st with messages := initMsgs ++ toPassthrough }
+    else
+      -- Failed. Put all the messages back on the message log and add an error
+      modify fun st => { st with messages := initMsgs ++ msgs }
+      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{res}"
+      pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
+  | _ => throwUnsupportedSyntax
+
+open CodeAction Server RequestM in
+/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
+@[command_code_action guardMsgsCmd]
+def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
+  let .node _ ts := node | return #[]
+  let res := ts.findSome? fun
+    | .node (.ofCustomInfo { stx, value }) _ => return (stx, (← value.get? GuardMsgFailure).res)
+    | _ => none
+  let some (stx, res) := res | return #[]
+  let doc ← readDoc
+  let eager := {
+    title := "Update #guard_msgs with tactic output"
+    kind? := "quickfix"
+    isPreferred? := true
+  }
+  pure #[{
+    eager
+    lazy? := some do
+      let some start := stx.getPos? true | return eager
+      let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
+      let newText := if res.isEmpty then
+        ""
+      else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?
+        s!"/-- {res} -/\n"
+      else
+        s!"/--\n{res}\n-/\n"
+      pure { eager with
+        edit? := some <|.ofTextEdit doc.versionedIdentifier {
+          range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩
+          newText
+        }
+      }
+  }]
+
+end Lean.Elab.Tactic.GuardMsgs
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index 46d86605c1..1a00994229 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -7,11 +7,7 @@ prelude
 import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Lean.Data.Json.Elab
-
-/-- Gets the LSP range from a `String.Range`. -/
-def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
+import Lean.Data.Lsp.Utf16
 
 /-!
 # "Try this" support
diff --git a/src/Lean/Server/CodeActions.lean b/src/Lean/Server/CodeActions.lean
index 7abe25819e..1a02fc26db 100644
--- a/src/Lean/Server/CodeActions.lean
+++ b/src/Lean/Server/CodeActions.lean
@@ -4,165 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: E.W.Ayers
 -/
-prelude
-import Lean.Server.FileWorker.RequestHandling
-import Lean.Server.InfoUtils
-
-namespace Lean.Server
-
-open Lsp
-open RequestM
-open Snapshots
-
-/-- 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`.
- -/
-structure LazyCodeAction where
-  /-- This is the initial code action that is sent to the server, to implement -/
-  eager : CodeAction
-  lazy? : Option (IO CodeAction) := none
-
-/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action. -/
-structure CodeActionResolveData where
-  params : CodeActionParams
-  /-- Name of CodeActionProvider that produced this request. -/
-  providerName : Name
-  /-- Index in the list of code action that the given provider generated. -/
-  providerResultIndex : Nat
-  deriving ToJson, FromJson
-
-def CodeAction.getFileSource! (ca : CodeAction) : DocumentUri :=
-  let r : Except String DocumentUri := do
-    let some data := ca.data?
-      | throw s!"no data param on code action {ca.title}"
-    let data : CodeActionResolveData ← fromJson? data
-    return data.params.textDocument.uri
-  match r with
-  | Except.ok uri => uri
-  | Except.error e => panic! e
-
-instance : FileSource CodeAction where
-  fileSource x := CodeAction.getFileSource! x
-
-
-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 `@[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.
--/
-def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
-deriving instance Inhabited for CodeActionProvider
-
-private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
-  IO.mkRef ∅
-
-def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
-  builtinCodeActionProviders.modify (·.insert decl provider)
-
-builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
-  addEntryFn := fun s n => s.insert n
-  toArrayFn  := fun es => es.toArray.qsort Name.quickLt
-}
-
-builtin_initialize
-  let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
-    name
-    descr           := (if builtin then "(builtin) " else "") ++
-      "Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
-    applicationTime := .afterCompilation
-    add             := fun decl stx kind => do
-      Attribute.Builtin.ensureNoArgs stx
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
-        throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
-      let env ← getEnv
-      if builtin then
-        let h := mkConst decl
-        declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
-      else
-        setEnv <| codeActionProviderExt.addEntry env decl
-  }
-  mkAttr true `builtin_code_action_provider
-  mkAttr false `code_action_provider
-
-private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
-  evalConstCheck CodeActionProvider ``CodeActionProvider declName
-
-/-- Get a `CodeActionProvider` from a declaration name. -/
-@[implemented_by evalCodeActionProviderUnsafe]
-private opaque evalCodeActionProvider [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider
-
-/-- Handles a `textDocument/codeAction` request.
-
-This is implemented by calling all of the registered `CodeActionProvider` functions.
-
-[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction). -/
-def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array CodeAction)) := do
-  let doc ← readDoc
-  let pos := doc.meta.text.lspPosToUtf8Pos params.range.end
-  withWaitFindSnap doc (fun s => s.endPos ≥ pos)
-    (notFoundX := return #[])
-    fun snap => do
-      let caps ← RequestM.runCoreM snap do
-        let env ← getEnv
-        let names := codeActionProviderExt.getState env |>.toArray
-        let caps ← names.mapM evalCodeActionProvider
-        return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
-      caps.concatMapM fun (providerName, cap) => do
-        let cas ← cap params snap
-        cas.mapIdxM fun i lca => do
-          if lca.lazy?.isNone then return lca.eager
-          let data : CodeActionResolveData := {
-            params, providerName, providerResultIndex := i
-          }
-          let j : Json := toJson data
-          let ca := { lca.eager with data? := some j }
-          return ca
-
-builtin_initialize
-  registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
-
-/-- Handler for `"codeAction/resolve"`.
-
-[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
--/
-def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAction) := do
-  let doc ← readDoc
-  let some data := param.data?
-    | throw (RequestError.invalidParams "Expected a data field on CodeAction.")
-  let data : CodeActionResolveData ← liftExcept <| Except.mapError RequestError.invalidParams <| fromJson? data
-  let pos := doc.meta.text.lspPosToUtf8Pos data.params.range.end
-  withWaitFindSnap doc (fun s => s.endPos ≥ pos)
-    (notFoundX := throw <| RequestError.internalError "snapshot not found")
-    fun snap => do
-      let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
-        | some cap => pure cap
-        | none     => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
-      let cas ← cap data.params snap
-      let some ca := cas[data.providerResultIndex]?
-        | throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
-      let some lazy := ca.lazy?
-        | throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
-      let r ← liftM lazy
-      return r
-
-builtin_initialize
-  registerLspRequestHandler "codeAction/resolve" CodeAction CodeAction handleCodeActionResolve
-
-end Lean.Server
+import Lean.Server.CodeActions.Attr
+import Lean.Server.CodeActions.Basic
+import Lean.Server.CodeActions.Provider
diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean
new file mode 100644
index 0000000000..a49e69d2a4
--- /dev/null
+++ b/src/Lean/Server/CodeActions/Attr.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Server.CodeActions.Basic
+
+/-!
+# Initial setup for code action attributes
+
+* Attribute `@[hole_code_action]` collects code actions which will be called
+  on each occurrence of a hole (`_`, `?_` or `sorry`).
+
+* Attribute `@[tactic_code_action]` collects code actions which will be called
+  on each occurrence of a tactic.
+
+* Attribute `@[command_code_action]` collects code actions which will be called
+  on each occurrence of a command.
+-/
+namespace Lean.CodeAction
+
+open Lean Elab Server Lsp RequestM Snapshots
+
+/-- A hole code action extension. -/
+abbrev HoleCodeAction :=
+  CodeActionParams → Snapshot →
+  (ctx : ContextInfo) → (hole : TermInfo) → RequestM (Array LazyCodeAction)
+
+/-- Read a hole code action from a declaration of the right type. -/
+def mkHoleCodeAction (n : Name) : ImportM HoleCodeAction := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck HoleCodeAction opts ``HoleCodeAction n
+
+/-- An extension which collects all the hole code actions. -/
+initialize holeCodeActionExt :
+    PersistentEnvExtension Name (Name × HoleCodeAction) (Array Name × Array HoleCodeAction) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure (#[], #[])
+    addImportedFn := fun as => return (#[], ← as.foldlM (init := #[]) fun m as =>
+      as.foldlM (init := m) fun m a => return m.push (← mkHoleCodeAction a))
+    addEntryFn := fun (s₁, s₂) (n₁, n₂) => (s₁.push n₁, s₂.push n₂)
+    exportEntriesFn := (·.1)
+  }
+
+initialize
+  registerBuiltinAttribute {
+    name := `hole_code_action
+    descr := "Declare a new hole code action, to appear in the code actions on ?_ and _"
+    applicationTime := .afterCompilation
+    add := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'hole_code_action', must be global"
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      modifyEnv (holeCodeActionExt.addEntry · (decl, ← mkHoleCodeAction decl))
+  }
+
+/-- A command code action extension. -/
+abbrev CommandCodeAction :=
+  CodeActionParams → Snapshot → (ctx : ContextInfo) → (node : InfoTree) →
+  RequestM (Array LazyCodeAction)
+
+/-- Read a command code action from a declaration of the right type. -/
+def mkCommandCodeAction (n : Name) : ImportM CommandCodeAction := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck CommandCodeAction opts ``CommandCodeAction n
+
+/-- An entry in the command code actions extension, containing the attribute arguments. -/
+structure CommandCodeActionEntry where
+  /-- The declaration to tag -/
+  declName : Name
+  /-- The command kinds that this extension supports.
+  If empty it is called on all command kinds. -/
+  cmdKinds : Array Name
+  deriving Inhabited
+
+/-- The state of the command code actions extension. -/
+structure CommandCodeActions where
+  /-- The list of command code actions to apply on any command. -/
+  onAnyCmd : Array CommandCodeAction := {}
+  /-- The list of command code actions to apply when a particular command kind is highlighted. -/
+  onCmd : NameMap (Array CommandCodeAction) := {}
+  deriving Inhabited
+
+/-- Insert a command code action entry into the `CommandCodeActions` structure. -/
+def CommandCodeActions.insert (self : CommandCodeActions)
+    (tacticKinds : Array Name) (action : CommandCodeAction) : CommandCodeActions :=
+  if tacticKinds.isEmpty then
+    { self with onAnyCmd := self.onAnyCmd.push action }
+  else
+    { self with onCmd := tacticKinds.foldl (init := self.onCmd) fun m a =>
+        m.insert a ((m.findD a #[]).push action) }
+
+/-- An extension which collects all the command code actions. -/
+initialize cmdCodeActionExt :
+    PersistentEnvExtension CommandCodeActionEntry (CommandCodeActionEntry × CommandCodeAction)
+      (Array CommandCodeActionEntry × CommandCodeActions) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure (#[], {})
+    addImportedFn := fun as => return (#[], ← as.foldlM (init := {}) fun m as =>
+      as.foldlM (init := m) fun m ⟨name, kinds⟩ =>
+        return m.insert kinds (← mkCommandCodeAction name))
+    addEntryFn := fun (s₁, s₂) (e, n₂) => (s₁.push e, s₂.insert e.cmdKinds n₂)
+    exportEntriesFn := (·.1)
+  }
+
+/--
+This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
+
+* `@[command_code_action kind]`: This is a code action which applies to applications of the command
+  `kind` (a command syntax kind), which can replace the command or insert things before or after it.
+
+* `@[command_code_action kind₁ kind₂]`: shorthand for
+  `@[command_code_action kind₁, command_code_action kind₂]`.
+
+* `@[command_code_action]`: This is a command code action that applies to all commands.
+  Use sparingly.
+-/
+syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
+
+initialize
+  registerBuiltinAttribute {
+    name := `command_code_action
+    descr := "Declare a new command code action, to appear in the code actions on commands"
+    applicationTime := .afterCompilation
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'command_code_action', must be global"
+      let `(attr| command_code_action $args*) := stx | return
+      let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
+  }
diff --git a/src/Lean/Server/CodeActions/Basic.lean b/src/Lean/Server/CodeActions/Basic.lean
new file mode 100644
index 0000000000..7abe25819e
--- /dev/null
+++ b/src/Lean/Server/CodeActions/Basic.lean
@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: E.W.Ayers
+-/
+prelude
+import Lean.Server.FileWorker.RequestHandling
+import Lean.Server.InfoUtils
+
+namespace Lean.Server
+
+open Lsp
+open RequestM
+open Snapshots
+
+/-- 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`.
+ -/
+structure LazyCodeAction where
+  /-- This is the initial code action that is sent to the server, to implement -/
+  eager : CodeAction
+  lazy? : Option (IO CodeAction) := none
+
+/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action. -/
+structure CodeActionResolveData where
+  params : CodeActionParams
+  /-- Name of CodeActionProvider that produced this request. -/
+  providerName : Name
+  /-- Index in the list of code action that the given provider generated. -/
+  providerResultIndex : Nat
+  deriving ToJson, FromJson
+
+def CodeAction.getFileSource! (ca : CodeAction) : DocumentUri :=
+  let r : Except String DocumentUri := do
+    let some data := ca.data?
+      | throw s!"no data param on code action {ca.title}"
+    let data : CodeActionResolveData ← fromJson? data
+    return data.params.textDocument.uri
+  match r with
+  | Except.ok uri => uri
+  | Except.error e => panic! e
+
+instance : FileSource CodeAction where
+  fileSource x := CodeAction.getFileSource! x
+
+
+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 `@[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.
+-/
+def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
+deriving instance Inhabited for CodeActionProvider
+
+private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
+  IO.mkRef ∅
+
+def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
+  builtinCodeActionProviders.modify (·.insert decl provider)
+
+builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
+  addEntryFn := fun s n => s.insert n
+  toArrayFn  := fun es => es.toArray.qsort Name.quickLt
+}
+
+builtin_initialize
+  let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
+    name
+    descr           := (if builtin then "(builtin) " else "") ++
+      "Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
+    applicationTime := .afterCompilation
+    add             := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
+        throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
+      let env ← getEnv
+      if builtin then
+        let h := mkConst decl
+        declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
+      else
+        setEnv <| codeActionProviderExt.addEntry env decl
+  }
+  mkAttr true `builtin_code_action_provider
+  mkAttr false `code_action_provider
+
+private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
+  evalConstCheck CodeActionProvider ``CodeActionProvider declName
+
+/-- Get a `CodeActionProvider` from a declaration name. -/
+@[implemented_by evalCodeActionProviderUnsafe]
+private opaque evalCodeActionProvider [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider
+
+/-- Handles a `textDocument/codeAction` request.
+
+This is implemented by calling all of the registered `CodeActionProvider` functions.
+
+[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction). -/
+def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array CodeAction)) := do
+  let doc ← readDoc
+  let pos := doc.meta.text.lspPosToUtf8Pos params.range.end
+  withWaitFindSnap doc (fun s => s.endPos ≥ pos)
+    (notFoundX := return #[])
+    fun snap => do
+      let caps ← RequestM.runCoreM snap do
+        let env ← getEnv
+        let names := codeActionProviderExt.getState env |>.toArray
+        let caps ← names.mapM evalCodeActionProvider
+        return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
+      caps.concatMapM fun (providerName, cap) => do
+        let cas ← cap params snap
+        cas.mapIdxM fun i lca => do
+          if lca.lazy?.isNone then return lca.eager
+          let data : CodeActionResolveData := {
+            params, providerName, providerResultIndex := i
+          }
+          let j : Json := toJson data
+          let ca := { lca.eager with data? := some j }
+          return ca
+
+builtin_initialize
+  registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
+
+/-- Handler for `"codeAction/resolve"`.
+
+[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
+-/
+def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAction) := do
+  let doc ← readDoc
+  let some data := param.data?
+    | throw (RequestError.invalidParams "Expected a data field on CodeAction.")
+  let data : CodeActionResolveData ← liftExcept <| Except.mapError RequestError.invalidParams <| fromJson? data
+  let pos := doc.meta.text.lspPosToUtf8Pos data.params.range.end
+  withWaitFindSnap doc (fun s => s.endPos ≥ pos)
+    (notFoundX := throw <| RequestError.internalError "snapshot not found")
+    fun snap => do
+      let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
+        | some cap => pure cap
+        | none     => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
+      let cas ← cap data.params snap
+      let some ca := cas[data.providerResultIndex]?
+        | throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
+      let some lazy := ca.lazy?
+        | throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
+      let r ← liftM lazy
+      return r
+
+builtin_initialize
+  registerLspRequestHandler "codeAction/resolve" CodeAction CodeAction handleCodeActionResolve
+
+end Lean.Server
diff --git a/src/Lean/Server/CodeActions/Provider.lean b/src/Lean/Server/CodeActions/Provider.lean
new file mode 100644
index 0000000000..ae0baa619f
--- /dev/null
+++ b/src/Lean/Server/CodeActions/Provider.lean
@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.BuiltinTerm
+import Lean.Elab.BuiltinNotation
+import Lean.Server.InfoUtils
+import Lean.Server.CodeActions.Attr
+
+/-!
+# 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.)
+-/
+namespace Lean.CodeAction
+
+open Lean Elab Term Server RequestM
+
+/--
+A code action which calls all `@[hole_code_action]` code actions on each hole
+(`?_`, `_`, or `sorry`).
+-/
+@[code_action_provider] def holeCodeActionProvider : CodeActionProvider := fun params snap => do
+  let doc ← readDoc
+  let startPos := doc.meta.text.lspPosToUtf8Pos params.range.start
+  let endPos := doc.meta.text.lspPosToUtf8Pos params.range.end
+  have holes := snap.infoTree.foldInfo (init := #[]) fun ctx info result => Id.run do
+    let .ofTermInfo info := info | result
+    unless [``elabHole, ``elabSyntheticHole, ``elabSorry].contains info.elaborator do
+      return result
+    let (some head, some tail) := (info.stx.getPos? true, info.stx.getTailPos? true) | result
+    unless head ≤ endPos && startPos ≤ tail do return result
+    result.push (ctx, info)
+  let #[(ctx, info)] := holes | return #[]
+  (holeCodeActionExt.getState snap.env).2.concatMapM (· params snap ctx info)
+
+/--
+The return value of `findTactic?`.
+This is the syntax for which code actions will be triggered.
+-/
+inductive FindTacticResult
+  /-- The nearest enclosing tactic is a tactic, with the given syntax stack. -/
+  | tactic : Syntax.Stack → 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`). -/
+  | tacticSeq : (preferred : Bool) → (insertIdx : Nat) → Syntax.Stack → 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 `tacticSeq`s" 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.
+-/
+partial def findTactic? (preferred : String.Pos → Bool) (range : String.Range)
+    (root : Syntax) : Option FindTacticResult := do _ ← visit root; ← go [] root
+where
+  /-- 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). -/
+  visit (stx : Syntax) (prev? : Option String.Pos := none) : Option Bool := do
+    let left ← stx.getPos? true
+    guard <| prev?.getD left ≤ range.start
+    let .original (endPos := right) (trailing := trailing) .. := stx.getTailInfo | none
+    guard <| right.byteIdx + trailing.bsize ≥ range.stop.byteIdx
+    return left ≤ range.start && right ≥ range.stop
+
+  /-- Merges the results of two `FindTacticResult`s. 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. -/
+  merge : (r₁ : Option FindTacticResult) → (r₂ : FindTacticResult) → FindTacticResult
+  | some r₁@(.tacticSeq (preferred := true) ..), .tacticSeq (preferred := false) .. => r₁
+  | _, r₂ => r₂
+
+  /-- 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. -/
+  go (stack : Syntax.Stack) (stx : Syntax) (prev? : Option String.Pos := none) :
+      Option (Option FindTacticResult) := do
+    if stx.getKind == ``Parser.Tactic.tacticSeq then
+      -- TODO: this implementation is a bit too strict about the beginning of tacticSeqs.
+      -- We would like to be able to parse
+      -- · |
+      --   foo
+      -- (where `|` is the cursor position) as an insertion into the sequence containing foo
+      -- at index 0, but we currently use the start of the tacticSeq, which is the foo token,
+      -- as the earliest possible location that will be associated to the sequence.
+      let bracket := stx[0].getKind == ``Parser.Tactic.tacticSeqBracketed
+      let argIdx := if bracket then 1 else 0
+      let (stack, stx) := ((stx[0], argIdx) :: (stx, 0) :: stack, stx[0][argIdx])
+      let mainRes := stx[0].getPos?.map fun pos =>
+        let i := Id.run do
+          for i in [0:stx.getNumArgs] do
+            if let some pos' := stx[2*i].getPos? then
+              if range.stop < pos' then
+                return i
+          (stx.getNumArgs + 1) / 2
+        .tacticSeq (bracket || preferred pos) i ((stx, 0) :: stack)
+      let mut childRes := none
+      for i in [0:stx.getNumArgs:2] do
+        if let some inner := visit stx[i] then
+          let stack := (stx, i) :: stack
+          if let some child := (← go stack stx[i]) <|>
+            (if inner then some (.tactic ((stx[i], 0) :: stack)) else none)
+          then
+            if childRes.isSome then failure
+            childRes := merge mainRes child
+      return childRes <|> mainRes
+    else
+      let mut childRes := none
+      let mut prev? := prev?
+      for i in [0:stx.getNumArgs] do
+        if let some _ := visit stx[i] prev? then
+          if let some child ← go ((stx, i) :: stack) stx[i] prev? then
+            if childRes.isSome then failure
+            childRes := child
+        prev? := stx[i].getTailPos? true <|> prev?
+      return childRes
+
+/--
+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.)
+-/
+partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
+  (ctx? : Option ContextInfo) (t : InfoTree)
+  (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
+    Option (ContextInfo × InfoTree) :=
+  match t with
+  | .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
+  | node@(.node i ts) => do
+    if let some ctx := ctx? then
+      if let some range := i.stx.getRange? canonicalOnly then
+        -- FIXME: info tree needs to be organized better so that this works
+        -- guard <| range.includes tgtRange
+        if i.stx.getKind == kind && range == tgtRange && f ctx i then
+          return (ctx, node)
+    for t in ts do
+      if let some res := findInfoTree? kind tgtRange (i.updateContext? ctx?) t f canonicalOnly then
+        return res
+    none
+  | _ => none
+
+/--
+A code action which calls all `@[command_code_action]` code actions on each command.
+-/
+@[code_action_provider] def cmdCodeActionProvider : CodeActionProvider := fun params snap => do
+  let doc ← readDoc
+  let startPos := doc.meta.text.lspPosToUtf8Pos params.range.start
+  let endPos := doc.meta.text.lspPosToUtf8Pos params.range.end
+  have cmds := snap.infoTree.foldInfoTree (init := #[]) fun ctx node result => Id.run do
+    let .node (.ofCommandInfo info) _ := node | result
+    let (some head, some tail) := (info.stx.getPos? true, info.stx.getTailPos? true) | result
+    unless head ≤ endPos && startPos ≤ tail do return result
+    result.push (ctx, node)
+  let actions := (cmdCodeActionExt.getState snap.env).2
+  let mut out := #[]
+  for (ctx, node) in cmds do
+    let .node (.ofCommandInfo info) _ := node | unreachable!
+    if let some arr := actions.onCmd.find? info.stx.getKind then
+      for act in arr do
+        try out := out ++ (← act params snap ctx node) catch _ => pure ()
+    for act in actions.onAnyCmd do
+      try out := out ++ (← act params snap ctx node) catch _ => pure ()
+  pure out
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
new file mode 100644
index 0000000000..c7e85438e1
--- /dev/null
+++ b/tests/lean/run/guard_msgs.lean
@@ -0,0 +1,51 @@
+#guard_msgs in
+/-- error: unknown identifier 'x' -/
+#guard_msgs in
+example : α := x
+
+/--
+error: unknown identifier 'x'
+---
+error: ❌ Docstring on `#guard_msgs` does not match generated message:
+
+error: unknown identifier 'x'
+-/
+#guard_msgs in
+#guard_msgs in
+example : α := x
+
+#guard_msgs in
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+example : α := sorry
+
+#guard_msgs in
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs(warning) in
+example : α := sorry
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+#guard_msgs(error) in
+example : α := sorry
+
+#guard_msgs in
+#guard_msgs(drop warning) in
+example : α := sorry
+
+#guard_msgs in
+#guard_msgs(error, drop warning) in
+example : α := sorry
+
+#guard_msgs in
+/-- error: unknown identifier 'x' -/
+#guard_msgs(error, drop warning) in
+example : α := x
+
+#guard_msgs in
+/--
+error: failed to synthesize instance
+  OfNat α 22
+-/
+#guard_msgs(error) in
+example : α := 22