From 8caa7744307aa790be1a32d3f0a1a2e75c54aa85 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 7 May 2023 21:16:51 -0400
Subject: [PATCH 1/8] feat: 'Try this' support

---
 Std.lean                 |   2 +
 Std/Lean/Name.lean       |  15 ++++++
 Std/Lean/Position.lean   |  14 +++++
 Std/Tactic/ShowTerm.lean |  10 +---
 Std/Tactic/TryThis.lean  | 111 ++++++++++++++++++++++++++++++++-------
 5 files changed, 125 insertions(+), 27 deletions(-)
 create mode 100644 Std/Lean/Name.lean
 create mode 100644 Std/Lean/Position.lean

diff --git a/Std.lean b/Std.lean
index cdca4e6396..b7da4cdca8 100644
--- a/Std.lean
+++ b/Std.lean
@@ -64,10 +64,12 @@ import Std.Lean.Meta.LCtx
 import Std.Lean.Meta.SavedState
 import Std.Lean.Meta.UnusedNames
 import Std.Lean.MonadBacktrack
+import Std.Lean.Name
 import Std.Lean.NameMapAttribute
 import Std.Lean.Parser
 import Std.Lean.PersistentHashMap
 import Std.Lean.PersistentHashSet
+import Std.Lean.Position
 import Std.Lean.Tactic
 import Std.Lean.TagAttribute
 import Std.Linter
diff --git a/Std/Lean/Name.lean b/Std/Lean/Name.lean
new file mode 100644
index 0000000000..f7d43568fa
--- /dev/null
+++ b/Std/Lean/Name.lean
@@ -0,0 +1,15 @@
+/-
+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
+
+namespace Lean.Name
+
+/-- Returns true if the name has any numeric components. -/
+def hasNum : Name → Bool
+  | .anonymous => false
+  | .str p _ => p.hasNum
+  | .num _ _ => true
diff --git a/Std/Lean/Position.lean b/Std/Lean/Position.lean
new file mode 100644
index 0000000000..d14095914c
--- /dev/null
+++ b/Std/Lean/Position.lean
@@ -0,0 +1,14 @@
+/-
+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.Data.Lsp.Utf16
+
+/-- Gets the LSP range from a pair of positions. -/
+def Lean.FileMap.utf8PosToLspRange (text : FileMap) (start «end» : String.Pos) : Lsp.Range :=
+  { start := text.utf8PosToLspPos start, «end» := text.utf8PosToLspPos «end» }
+
+/-- Gets the LSP range of syntax `stx`. -/
+def Lean.FileMap.rangeOfStx? (text : FileMap) (stx : Syntax) : Option Lsp.Range :=
+  return text.utf8PosToLspRange (← stx.getPos?) (← stx.getTailPos?)
diff --git a/Std/Tactic/ShowTerm.lean b/Std/Tactic/ShowTerm.lean
index fe78716156..459c3d3312 100644
--- a/Std/Tactic/ShowTerm.lean
+++ b/Std/Tactic/ShowTerm.lean
@@ -18,10 +18,7 @@ open Lean Elab Tactic TryThis
 elab (name := showTermTac) tk:"show_term " t:tacticSeq : tactic => withMainContext do
   let g ← getMainGoal
   evalTactic t
-  -- TODO: At the moment it is more useful to use an Expr MessageData
-  -- instead of a Syntax because the former is clickable in the infoview
-  -- addExactSuggestion tk (← instantiateMVars (mkMVar g)).headBeta
-  logInfoAt tk (← instantiateMVars (mkMVar g)).headBeta
+  addExactSuggestion tk (← instantiateMVars (mkMVar g)).headBeta (ref? := ← getRef)
 
 /--
 `show_term e` elaborates `e`, then prints the generated term.
@@ -31,8 +28,5 @@ elab (name := showTermTac) tk:"show_term " t:tacticSeq : tactic => withMainConte
 elab (name := showTerm) tk:"show_term " t:term : term <= ty => do
   let e ← Term.elabTermEnsuringType t ty
   Term.synthesizeSyntheticMVarsNoPostponing
-  -- TODO: At the moment it is more useful to use an Expr MessageData
-  -- instead of a Syntax because the former is clickable in the infoview
-  -- addTermSuggestion tk (← instantiateMVars e).headBeta
-  logInfoAt tk (← instantiateMVars e).headBeta
+  addTermSuggestion tk (← instantiateMVars e).headBeta (ref? := ← getRef)
   pure e
diff --git a/Std/Tactic/TryThis.lean b/Std/Tactic/TryThis.lean
index 278844eb68..b42b93807a 100644
--- a/Std/Tactic/TryThis.lean
+++ b/Std/Tactic/TryThis.lean
@@ -1,42 +1,115 @@
 /-
 Copyright (c) 2021 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
+Authors: Gabriel Ebner, Mario Carneiro
 -/
-import Lean.PrettyPrinter.Delaborator.Basic
+import Lean.Server.CodeActions
+import Lean.Widget.UserWidget
+import Std.Lean.Name
+import Std.Lean.Position
 
 /-!
-# Stub for try-this support
+# "Try this" support
 
-Lean 4 does not yet support code actions
-to present tactic suggestions in the editor.
-This file contains a preliminary API
-that tactics can call to show suggestions.
+This implements a mechanism for tactics to print a message saying `Try this: <suggestion>`,
+where `<suggestion>` is a link to a replacement tactic. Users can either click on the link
+in the suggestion (provided by a widget), or use a code action which applies the suggestion.
 -/
 namespace Std.Tactic.TryThis
 
-open Lean Elab Elab.Tactic PrettyPrinter Meta
+open Lean Elab Elab.Tactic PrettyPrinter Meta Server Lsp RequestM
+
+/-- An info-tree data node corresponding to an application of the "Try this" command. -/
+structure TryThisInfo where
+  /-- The suggested replacement for this syntax, usually the rendering of another tactic syntax. -/
+  suggestion : String
+  /-- This is the span to replace with `suggestion`. If not supplied it will default to
+  the span of the syntax on which this info node is placed. -/
+  span? : Option (String.Pos × String.Pos) := none
+  deriving TypeName
+
+/--
+This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to
+apply the replacement.
+-/
+@[codeActionProvider] def tryThisProvider : 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
+  pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do
+    let .ofCustomInfo info := info | result
+    let some tti := info.value.get? TryThisInfo | result
+    let some (head, tail) := (tti.span? <|> return (← info.stx.getPos?, ← info.stx.getTailPos?))
+      | result
+    unless head ≤ endPos && startPos ≤ tail do return result
+    result.push {
+      eager.title := "Apply 'Try this'"
+      eager.kind? := "refactor"
+      eager.edit? := WorkspaceEdit.ofTextEdit params.textDocument.uri {
+        range := doc.meta.text.utf8PosToLspRange head tail
+        newText := tti.suggestion
+      }
+    }
+
+/--
+This is a widget which is placed by `TryThis.addSuggestion`; it says `Try this: <replacement>`
+where `<replacement>` is a link which will perform the replacement.
+-/
+@[widget] def tryThisWidget : Widget.UserWidgetDefinition where
+  name := "Tactic replacement"
+  javascript := "
+import * as React from 'react';
+import { EditorContext } from '@leanprover/infoview';
+const e = React.createElement;
+export default function(props) {
+  const editorConnection = React.useContext(EditorContext)
+  function onClick() {
+    editorConnection.api.applyEdit({
+      changes: { [props.pos.uri]: [{ range: props.range, newText: props.suggestion }] }
+    })
+  }
+  return e('div', {className: 'ml1'}, e('pre', {className: 'font-code pre-wrap'},
+    ['Try this: ', e('a', {onClick, title: 'Apply suggestion'}, props.suggestion)]))
+}"
 
 /-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/
 partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m]
     (s : Syntax) : m Syntax :=
-  s.replaceM fun s => if let `(?$_:ident) := s then `(?_) else pure none
+  s.replaceM fun s => do
+    let `(?$id:ident) := s | pure none
+    if id.getId.hasNum || id.getId.isInternal then `(?_) else pure none
 
 /-- Delaborate `e` into an expression suitable for use in `refine`. -/
 def delabToRefinableSyntax (e : Expr) : TermElabM Term :=
   return ⟨← replaceMVarsByUnderscores (← delab e)⟩
 
-/-- Add a "try this" suggestion. (TODO: this depends on code action support) -/
-def addSuggestion [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
-    (origStx : Syntax) (suggestion : Syntax) : m Unit :=
-  logInfoAt origStx m!"{suggestion}"
+/-- Add a "try this" suggestion. -/
+def addSuggestion (origStx : Syntax) {kind : Name} (suggestion : TSyntax kind)
+    (suggestionForMessage : Option MessageData := none)
+    (ref? : Option Syntax := none) : MetaM Unit := do
+  logInfoAt origStx m!"Try this: {suggestionForMessage.getD suggestion}"
+  -- TODO: use the right indentation
+  let text := Format.pretty (← PrettyPrinter.ppCategory kind suggestion)
+  let span? := do let e ← ref?; pure (← e.getPos?, ← e.getTailPos?)
+  pushInfoLeaf <| .ofCustomInfo {
+    stx := origStx
+    value := Dynamic.mk (TryThisInfo.mk text span?)
+  }
+  if let some (head, tail) := span? <|> return (← origStx.getPos?, ← origStx.getTailPos?) then
+    let map ← getFileMap
+    let range := Lsp.Range.mk (map.utf8PosToLspPos head) (map.utf8PosToLspPos tail)
+    let json := Json.mkObj [("suggestion", text), ("range", toJson range)]
+    Widget.saveWidgetInfo ``tryThisWidget json origStx
 
-/-- Add a `exact e` or `refine e` suggestion. (TODO: this depends on code action support) -/
-def addExactSuggestion (origTac : Syntax) (e : Expr) : TermElabM Unit := do
+/-- Add a `exact e` or `refine e` suggestion. -/
+def addExactSuggestion (origTac : Syntax) (e : Expr)
+    (ref? : Option Syntax := none) : TermElabM Unit := do
   let stx ← delabToRefinableSyntax e
   let tac ← if e.hasExprMVar then `(tactic| refine $stx) else `(tactic| exact $stx)
-  addSuggestion origTac tac
+  let msg := if e.hasExprMVar then m!"refine {e}" else m!"exact {e}"
+  addSuggestion origTac tac (suggestionForMessage := msg) (ref? := ref?)
 
-/-- Add a term suggestion. (TODO: this depends on code action support) -/
-def addTermSuggestion (origTerm : Syntax) (e : Expr) : TermElabM Unit := do
-  addSuggestion origTerm (← delabToRefinableSyntax e)
+/-- Add a term suggestion. -/
+def addTermSuggestion (origTerm : Syntax) (e : Expr)
+    (ref? : Option Syntax := none) : TermElabM Unit := do
+  addSuggestion origTerm (← delabToRefinableSyntax e) (suggestionForMessage := e) (ref? := ref?)

From 939c3058d3064c9c183b4e42faf398f5017203fd Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 8 May 2023 04:13:12 -0400
Subject: [PATCH 2/8] feat: hole commands

---
 Std.lean                               |   4 +
 Std/Tactic/HoleCommand.lean            |   3 +
 Std/Tactic/HoleCommand/Attr.lean       |  52 ++++++++++
 Std/Tactic/HoleCommand/CodeAction.lean |  37 +++++++
 Std/Tactic/HoleCommand/Misc.lean       | 130 +++++++++++++++++++++++++
 5 files changed, 226 insertions(+)
 create mode 100644 Std/Tactic/HoleCommand.lean
 create mode 100644 Std/Tactic/HoleCommand/Attr.lean
 create mode 100644 Std/Tactic/HoleCommand/CodeAction.lean
 create mode 100644 Std/Tactic/HoleCommand/Misc.lean

diff --git a/Std.lean b/Std.lean
index b7da4cdca8..c3c1077556 100644
--- a/Std.lean
+++ b/Std.lean
@@ -84,6 +84,10 @@ import Std.Tactic.Ext
 import Std.Tactic.Ext.Attr
 import Std.Tactic.GuardExpr
 import Std.Tactic.HaveI
+import Std.Tactic.HoleCommand
+import Std.Tactic.HoleCommand.Attr
+import Std.Tactic.HoleCommand.CodeAction
+import Std.Tactic.HoleCommand.Misc
 import Std.Tactic.Lint
 import Std.Tactic.Lint.Basic
 import Std.Tactic.Lint.Frontend
diff --git a/Std/Tactic/HoleCommand.lean b/Std/Tactic/HoleCommand.lean
new file mode 100644
index 0000000000..189cbcfd5d
--- /dev/null
+++ b/Std/Tactic/HoleCommand.lean
@@ -0,0 +1,3 @@
+import Std.Tactic.HoleCommand.Attr
+import Std.Tactic.HoleCommand.CodeAction
+import Std.Tactic.HoleCommand.Misc
diff --git a/Std/Tactic/HoleCommand/Attr.lean b/Std/Tactic/HoleCommand/Attr.lean
new file mode 100644
index 0000000000..1a88e227fa
--- /dev/null
+++ b/Std/Tactic/HoleCommand/Attr.lean
@@ -0,0 +1,52 @@
+/-
+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
+import Std.Util.TermUnsafe
+
+/-!
+# Initial setup for hole commands
+
+This declares an attribute `@[hole_command]` which collects code actions which will be called
+on each occurrence of a hole (`_`, `?_` or `sorry`).
+-/
+namespace Std.Tactic
+
+open Lean Elab Server Lsp RequestM Snapshots
+
+/-- A hole command extension. -/
+abbrev HoleCommand :=
+  CodeActionParams → Snapshot → (hole : TermInfo) → RequestM (Array LazyCodeAction)
+
+namespace HoleCommand
+
+/-- Read a `positivity` extension from a declaration of the right type. -/
+def mkHoleCommand (n : Name) : ImportM HoleCommand := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck HoleCommand opts ``HoleCommand n
+
+/-- An extension which collects all the hole commands. -/
+initialize holeCommandExt :
+    PersistentEnvExtension Name (Name × HoleCommand) (Array Name × Array HoleCommand) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure (#[], #[])
+    addImportedFn := fun as => return (#[], ← as.foldlM (init := #[]) fun m as =>
+      as.foldlM (init := m) fun m a => return m.push (← mkHoleCommand a))
+    addEntryFn := fun (s₁, s₂) (n₁, n₂) => (s₁.push n₁, s₂.push n₂)
+    exportEntriesFn := (·.1)
+  }
+
+initialize
+  registerBuiltinAttribute {
+    name := `hole_command
+    descr := "Declare a new hole command, 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_command', must be global"
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      modifyEnv (holeCommandExt.addEntry · (decl, ← mkHoleCommand decl))
+  }
diff --git a/Std/Tactic/HoleCommand/CodeAction.lean b/Std/Tactic/HoleCommand/CodeAction.lean
new file mode 100644
index 0000000000..45b764761f
--- /dev/null
+++ b/Std/Tactic/HoleCommand/CodeAction.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Std.Lean.Name
+import Std.Tactic.HoleCommand.Attr
+
+/-!
+# Initial setup for hole commands
+
+This declares a code action provider that calls all `@[hole_command]` definitions
+on each occurrence of a hole (`_`, `?_` or `sorry`).
+
+(This is in a separate file from `Std.Tactic.HoleCommand.Attr` so that the server does not attempt
+to use this code action provider when browsing the `Std.Tactic.HoleCommand.Attr` file itself.)
+-/
+namespace Std.Tactic.HoleCommand
+
+open Lean Elab.Term Server RequestM
+
+/--
+A code action which calls all `@[hole_command]` code actions on each hole (`?_`, `_`, or `sorry`).
+-/
+@[codeActionProvider] def holeCommandProvider : 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?, info.stx.getTailPos?) | result
+    unless head ≤ endPos && startPos ≤ tail do return result
+    result.push info
+  let #[info] := holes | return #[]
+  (holeCommandExt.getState snap.env).2.concatMapM (· params snap info)
diff --git a/Std/Tactic/HoleCommand/Misc.lean b/Std/Tactic/HoleCommand/Misc.lean
new file mode 100644
index 0000000000..578617ef47
--- /dev/null
+++ b/Std/Tactic/HoleCommand/Misc.lean
@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Std.Lean.Position
+import Std.Tactic.HoleCommand.CodeAction
+
+/-!
+# Miscellaneous hole commands
+
+This declares some basic hole commands, using the `@[hole_command]` API.
+-/
+namespace Std.Tactic.HoleCommand
+
+open Lean Server RequestM Meta
+
+/--
+Hole command used to fill in a structure's field when specifying an instance.
+
+In the following:
+
+```lean
+instance : Monad Id := _
+```
+
+invoking the hole command "Generate a skeleton for the structure under construction." produces:
+
+```lean
+instance : Monad Id := {
+  map := _
+  mapConst := _
+  pure := _
+  seq := _
+  seqLeft := _
+  seqRight := _
+  bind := _
+}
+```
+-/
+@[hole_command] partial def instanceStub : HoleCommand := fun params snap info => do
+  let some ty := info.expectedType? | return #[]
+  let .const name _ := (← runTermElabM snap (whnf ty)).getAppFn | return #[]
+  unless isStructure snap.env name do return #[]
+  let eager := {
+    title := "Generate a skeleton for the structure under construction."
+    kind? := "quickfix"
+    isPreferred? := true
+  }
+  let doc ← readDoc
+  pure #[{
+    eager
+    lazy? := some do
+      let mut str := "{" -- TODO: use the right indentation
+      for field in collectFields snap.env name #[] do
+        str := str ++ s!"\n  {field} := _"
+      str := str ++ s!"\n}"
+      pure { eager with
+        edit? := some <| .ofTextEdit params.textDocument.uri {
+          range := (doc.meta.text.rangeOfStx? info.stx).get!
+          newText := str
+        }
+      }
+  }]
+where
+  /-- Returns the fields of a structure, unfolding parent structures. -/
+  collectFields (env : Environment) (structName : Name) (fields : Array Name) : Array Name :=
+    (getStructureFields env structName).foldl (init := fields) fun fields field =>
+      match isSubobjectField? env structName field with
+      | some substructName => collectFields env substructName fields
+      | none => fields.push field
+
+/--
+Invoking hole command "Generate a list of equations for a recursive definition" in the following:
+
+```lean
+def foo : Expr → Unit := _
+```
+
+produces:
+
+```lean
+def foo : Expr → Unit := fun
+  | .bvar deBruijnIndex => _
+  | .fvar fvarId => _
+  | .mvar mvarId => _
+  | .sort u => _
+  | .const declName us => _
+  | .app fn arg => _
+  | .lam binderName binderType body binderInfo => _
+  | .forallE binderName binderType body binderInfo => _
+  | .letE declName type value body nonDep => _
+  | .lit _ => _
+  | .mdata data expr => _
+  | .proj typeName idx struct => _
+```
+
+-/
+@[hole_command] def eqnStub : HoleCommand := fun params snap info => do
+  let some ty := info.expectedType? | return #[]
+  let .forallE _ dom .. ← runTermElabM snap (whnf ty) | return #[]
+  let .const name _ := (← runTermElabM snap (whnf dom)).getAppFn | return #[]
+  let some (.inductInfo val) := snap.env.find? name | return #[]
+  let eager := {
+    title := "Generate a list of equations for a recursive definition."
+    kind? := "quickfix"
+  }
+  let doc ← readDoc
+  pure #[{
+    eager
+    lazy? := some do
+      let mut str := "fun" -- TODO: use the right indentation
+      for ctor in val.ctors do
+        let some (.ctorInfo ci) := snap.env.find? ctor | panic! "bad inductive"
+        str := str ++ s!"\n  | .{ctor.updatePrefix .anonymous}"
+        for arg in getArgs ci.type #[] do
+          str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
+        str := str ++ s!" => _"
+      pure { eager with
+        edit? := some <|.ofTextEdit params.textDocument.uri {
+          range := (doc.meta.text.rangeOfStx? info.stx).get!
+          newText := str
+        }
+      }
+  }]
+where
+  /-- Returns the explicit arguments given a type. -/
+  getArgs : Expr → Array Name → Array Name
+  | .forallE n _ body bi, args => getArgs body <| if bi.isExplicit then args.push n else args
+  | _, args => args

From 95304e1a2116b317d37be3af8f1618742ed0261c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 8 May 2023 07:15:11 -0400
Subject: [PATCH 3/8] feat: improved indentation

---
 Std.lean                               |  1 +
 Std/Lean/Format.lean                   | 19 +++++++++
 Std/Lean/Name.lean                     |  2 -
 Std/Lean/Position.lean                 |  6 +++
 Std/Tactic/HoleCommand/Attr.lean       |  3 +-
 Std/Tactic/HoleCommand/CodeAction.lean | 12 +++---
 Std/Tactic/HoleCommand/Misc.lean       | 59 ++++++++++++++++++++------
 Std/Tactic/TryThis.lean                | 15 +++++--
 8 files changed, 93 insertions(+), 24 deletions(-)
 create mode 100644 Std/Lean/Format.lean

diff --git a/Std.lean b/Std.lean
index c3c1077556..799adacd61 100644
--- a/Std.lean
+++ b/Std.lean
@@ -51,6 +51,7 @@ import Std.Lean.AttributeExtra
 import Std.Lean.Command
 import Std.Lean.Delaborator
 import Std.Lean.Expr
+import Std.Lean.Format
 import Std.Lean.HashMap
 import Std.Lean.HashSet
 import Std.Lean.Meta.AssertHypotheses
diff --git a/Std/Lean/Format.lean b/Std/Lean/Format.lean
new file mode 100644
index 0000000000..3f23b01d72
--- /dev/null
+++ b/Std/Lean/Format.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Std.Tactic.OpenPrivate
+
+namespace Std.Format
+
+open private State State.mk State.out from Init.Data.Format.Basic in
+/--
+Renders a `Format` to a string. Similar to `Format.pretty`, but with additional options:
+* `w`: the total width
+* `indent`: the initial indentation
+* `column`: the initial column for the first line
+-/
+def prettyExtra (f : Format) (w : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
+  let act : StateM State Unit := prettyM f w indent
+  State.out <| act (State.mk "" column) |>.snd
diff --git a/Std/Lean/Name.lean b/Std/Lean/Name.lean
index f7d43568fa..f157cfcd10 100644
--- a/Std/Lean/Name.lean
+++ b/Std/Lean/Name.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
-import Lean
-
 namespace Lean.Name
 
 /-- Returns true if the name has any numeric components. -/
diff --git a/Std/Lean/Position.lean b/Std/Lean/Position.lean
index d14095914c..1bc4634d90 100644
--- a/Std/Lean/Position.lean
+++ b/Std/Lean/Position.lean
@@ -12,3 +12,9 @@ def Lean.FileMap.utf8PosToLspRange (text : FileMap) (start «end» : String.Pos)
 /-- Gets the LSP range of syntax `stx`. -/
 def Lean.FileMap.rangeOfStx? (text : FileMap) (stx : Syntax) : Option Lsp.Range :=
   return text.utf8PosToLspRange (← stx.getPos?) (← stx.getTailPos?)
+
+/-- Return the beginning of the line contatining character `pos`. -/
+def Lean.findLineStart (s : String) (pos : String.Pos) : String.Pos :=
+  match s.revFindAux (· = '\n') pos with
+  | none => 0
+  | some n => ⟨n.byteIdx + 1⟩
diff --git a/Std/Tactic/HoleCommand/Attr.lean b/Std/Tactic/HoleCommand/Attr.lean
index 1a88e227fa..1ed9514941 100644
--- a/Std/Tactic/HoleCommand/Attr.lean
+++ b/Std/Tactic/HoleCommand/Attr.lean
@@ -18,7 +18,8 @@ open Lean Elab Server Lsp RequestM Snapshots
 
 /-- A hole command extension. -/
 abbrev HoleCommand :=
-  CodeActionParams → Snapshot → (hole : TermInfo) → RequestM (Array LazyCodeAction)
+  CodeActionParams → Snapshot →
+  (ctx : ContextInfo) → (hole : TermInfo) → RequestM (Array LazyCodeAction)
 
 namespace HoleCommand
 
diff --git a/Std/Tactic/HoleCommand/CodeAction.lean b/Std/Tactic/HoleCommand/CodeAction.lean
index 45b764761f..0c1c6218b6 100644
--- a/Std/Tactic/HoleCommand/CodeAction.lean
+++ b/Std/Tactic/HoleCommand/CodeAction.lean
@@ -3,6 +3,8 @@ 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 Std.Lean.Name
 import Std.Tactic.HoleCommand.Attr
 
@@ -26,12 +28,12 @@ A code action which calls all `@[hole_command]` code actions on each hole (`?_`,
   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
+  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?, info.stx.getTailPos?) | 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 info
-  let #[info] := holes | return #[]
-  (holeCommandExt.getState snap.env).2.concatMapM (· params snap info)
+    result.push (ctx, info)
+  let #[(ctx, info)] := holes | return #[]
+  (holeCommandExt.getState snap.env).2.concatMapM (· params snap ctx info)
diff --git a/Std/Tactic/HoleCommand/Misc.lean b/Std/Tactic/HoleCommand/Misc.lean
index 578617ef47..70e2285312 100644
--- a/Std/Tactic/HoleCommand/Misc.lean
+++ b/Std/Tactic/HoleCommand/Misc.lean
@@ -15,6 +15,21 @@ namespace Std.Tactic.HoleCommand
 
 open Lean Server RequestM Meta
 
+/-- Return the syntax stack leading to `target` from `root`, if one exists. -/
+def findStack? (root target : Syntax) : Option Syntax.Stack := do
+  let range ← target.getRange?
+  root.findStack? (·.getRange?.any (·.includes range))
+    (fun s => s.getKind == target.getKind && s.getRange? == range)
+
+/--
+Return the indentation (number of leading spaces) of the line containing `pos`,
+and whether `pos` is the first non-whitespace character in the line.
+-/
+def findIndentAndIsStart (s : String) (pos : String.Pos) : Nat × Bool :=
+  let start := findLineStart s pos
+  let body := s.findAux (· ≠ ' ') pos start
+  ((body - start).1, body == pos)
+
 /--
 Hole command used to fill in a structure's field when specifying an instance.
 
@@ -38,9 +53,9 @@ instance : Monad Id := {
 }
 ```
 -/
-@[hole_command] partial def instanceStub : HoleCommand := fun params snap info => do
+@[hole_command] partial def instanceStub : HoleCommand := fun params snap ctx info => do
   let some ty := info.expectedType? | return #[]
-  let .const name _ := (← runTermElabM snap (whnf ty)).getAppFn | return #[]
+  let .const name _ := (← info.runMetaM ctx (whnf ty)).getAppFn | return #[]
   unless isStructure snap.env name do return #[]
   let eager := {
     title := "Generate a skeleton for the structure under construction."
@@ -51,13 +66,30 @@ instance : Monad Id := {
   pure #[{
     eager
     lazy? := some do
-      let mut str := "{" -- TODO: use the right indentation
+      let useWhere := do
+        let _ :: (stx, _) :: _ ← findStack? snap.stx info.stx | none
+        guard (stx.getKind == ``Parser.Command.declValSimple)
+        stx[0].getPos?
+      let holePos := useWhere.getD info.stx.getPos?.get!
+      let (indent, isStart) := findIndentAndIsStart doc.meta.text.source holePos
+      let indent := "\n".pushn ' ' indent
+      let mut str := if useWhere.isSome then "where" else "{"
+      let mut first := useWhere.isNone && isStart
       for field in collectFields snap.env name #[] do
-        str := str ++ s!"\n  {field} := _"
-      str := str ++ s!"\n}"
+        if first then
+          str := str ++ " "
+          first := false
+        else
+          str := str ++ indent ++ "  "
+        str := str ++ s!"{field} := _"
+      if useWhere.isNone then
+        if isStart then
+          str := str ++ " }"
+        else
+          str := str ++ indent ++ "}"
       pure { eager with
         edit? := some <| .ofTextEdit params.textDocument.uri {
-          range := (doc.meta.text.rangeOfStx? info.stx).get!
+          range := doc.meta.text.utf8PosToLspRange holePos info.stx.getTailPos?.get!
           newText := str
         }
       }
@@ -96,10 +128,10 @@ def foo : Expr → Unit := fun
 ```
 
 -/
-@[hole_command] def eqnStub : HoleCommand := fun params snap info => do
+@[hole_command] def eqnStub : HoleCommand := fun params snap ctx info => do
   let some ty := info.expectedType? | return #[]
-  let .forallE _ dom .. ← runTermElabM snap (whnf ty) | return #[]
-  let .const name _ := (← runTermElabM snap (whnf dom)).getAppFn | return #[]
+  let .forallE _ dom .. ← info.runMetaM ctx (whnf ty) | return #[]
+  let .const name _ := (← info.runMetaM ctx (whnf dom)).getAppFn | return #[]
   let some (.inductInfo val) := snap.env.find? name | return #[]
   let eager := {
     title := "Generate a list of equations for a recursive definition."
@@ -109,16 +141,19 @@ def foo : Expr → Unit := fun
   pure #[{
     eager
     lazy? := some do
-      let mut str := "fun" -- TODO: use the right indentation
+      let holePos := info.stx.getPos?.get!
+      let (indent, isStart) := findIndentAndIsStart doc.meta.text.source holePos
+      let mut str := "fun"
+      let indent := "\n".pushn ' ' (if isStart then indent else indent + 2)
       for ctor in val.ctors do
         let some (.ctorInfo ci) := snap.env.find? ctor | panic! "bad inductive"
-        str := str ++ s!"\n  | .{ctor.updatePrefix .anonymous}"
+        str := str ++ indent ++ s!"| .{ctor.updatePrefix .anonymous}"
         for arg in getArgs ci.type #[] do
           str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
         str := str ++ s!" => _"
       pure { eager with
         edit? := some <|.ofTextEdit params.textDocument.uri {
-          range := (doc.meta.text.rangeOfStx? info.stx).get!
+          range := doc.meta.text.utf8PosToLspRange holePos info.stx.getTailPos?.get!
           newText := str
         }
       }
diff --git a/Std/Tactic/TryThis.lean b/Std/Tactic/TryThis.lean
index b42b93807a..e27297f4f3 100644
--- a/Std/Tactic/TryThis.lean
+++ b/Std/Tactic/TryThis.lean
@@ -6,6 +6,7 @@ Authors: Gabriel Ebner, Mario Carneiro
 import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Std.Lean.Name
+import Std.Lean.Format
 import Std.Lean.Position
 
 /-!
@@ -88,15 +89,21 @@ def addSuggestion (origStx : Syntax) {kind : Name} (suggestion : TSyntax kind)
     (suggestionForMessage : Option MessageData := none)
     (ref? : Option Syntax := none) : MetaM Unit := do
   logInfoAt origStx m!"Try this: {suggestionForMessage.getD suggestion}"
-  -- TODO: use the right indentation
-  let text := Format.pretty (← PrettyPrinter.ppCategory kind suggestion)
+  let map ← getFileMap
   let span? := do let e ← ref?; pure (← e.getPos?, ← e.getTailPos?)
+  let span?' := span? <|> return (← origStx.getPos?, ← origStx.getTailPos?)
+  let text ← PrettyPrinter.ppCategory kind suggestion
+  let (indent, column) := if let some (pos, _) := span?' then
+    let start := findLineStart map.source pos
+    let body := map.source.findAux (· ≠ ' ') pos start
+    ((body - start).1, (pos - start).1)
+  else (0, 0)
+  let text := Format.prettyExtra text (indent := indent) (column := column)
   pushInfoLeaf <| .ofCustomInfo {
     stx := origStx
     value := Dynamic.mk (TryThisInfo.mk text span?)
   }
-  if let some (head, tail) := span? <|> return (← origStx.getPos?, ← origStx.getTailPos?) then
-    let map ← getFileMap
+  if let some (head, tail) := span?' then
     let range := Lsp.Range.mk (map.utf8PosToLspPos head) (map.utf8PosToLspPos tail)
     let json := Json.mkObj [("suggestion", text), ("range", toJson range)]
     Widget.saveWidgetInfo ``tryThisWidget json origStx

From c6cb0e81f9eaa9aed0ad1f244a88469851630902 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 8 May 2023 08:18:08 -0400
Subject: [PATCH 4/8] feat: preserve hole kind in branches

---
 Std/Tactic/HoleCommand/Misc.lean | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/Std/Tactic/HoleCommand/Misc.lean b/Std/Tactic/HoleCommand/Misc.lean
index 70e2285312..868dcba5c5 100644
--- a/Std/Tactic/HoleCommand/Misc.lean
+++ b/Std/Tactic/HoleCommand/Misc.lean
@@ -30,6 +30,12 @@ def findIndentAndIsStart (s : String) (pos : String.Pos) : Nat × Bool :=
   let body := s.findAux (· ≠ ' ') pos start
   ((body - start).1, body == pos)
 
+/-- Constructs a hole with a kind matching the provided hole elaborator.  -/
+def holeKindToHoleString : (elaborator : Name) → (synthName : String) → String
+  | ``Elab.Term.elabSyntheticHole, name => "?" ++ name
+  | ``Elab.Term.elabSorry, _ => "sorry"
+  | _, _ => "_"
+
 /--
 Hole command used to fill in a structure's field when specifying an instance.
 
@@ -81,7 +87,8 @@ instance : Monad Id := {
           first := false
         else
           str := str ++ indent ++ "  "
-        str := str ++ s!"{field} := _"
+        let field := toString field
+        str := str ++ s!"{field} := {holeKindToHoleString info.elaborator field}"
       if useWhere.isNone then
         if isStart then
           str := str ++ " }"
@@ -147,10 +154,11 @@ def foo : Expr → Unit := fun
       let indent := "\n".pushn ' ' (if isStart then indent else indent + 2)
       for ctor in val.ctors do
         let some (.ctorInfo ci) := snap.env.find? ctor | panic! "bad inductive"
-        str := str ++ indent ++ s!"| .{ctor.updatePrefix .anonymous}"
+        let ctor := toString (ctor.updatePrefix .anonymous)
+        str := str ++ indent ++ s!"| .{ctor}"
         for arg in getArgs ci.type #[] do
           str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
-        str := str ++ s!" => _"
+        str := str ++ s!" => {holeKindToHoleString info.elaborator ctor}"
       pure { eager with
         edit? := some <|.ofTextEdit params.textDocument.uri {
           range := doc.meta.text.utf8PosToLspRange holePos info.stx.getTailPos?.get!

From 9d70feb598bf2d6e9cc335327dbba7a4163c6fc6 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 8 May 2023 15:21:23 -0400
Subject: [PATCH 5/8] refactor: move to `Std.CodeAction`, rename

---
 Std.lean                                      |  9 +++---
 Std/CodeAction.lean                           |  1 +
 Std/CodeAction/Hole.lean                      |  3 ++
 .../HoleCommand => CodeAction/Hole}/Attr.lean | 32 +++++++++----------
 .../Hole/Basic.lean}                          | 19 +++++------
 .../HoleCommand => CodeAction/Hole}/Misc.lean | 22 ++++++-------
 Std/Tactic/HoleCommand.lean                   |  3 --
 7 files changed, 44 insertions(+), 45 deletions(-)
 create mode 100644 Std/CodeAction.lean
 create mode 100644 Std/CodeAction/Hole.lean
 rename Std/{Tactic/HoleCommand => CodeAction/Hole}/Attr.lean (56%)
 rename Std/{Tactic/HoleCommand/CodeAction.lean => CodeAction/Hole/Basic.lean} (59%)
 rename Std/{Tactic/HoleCommand => CodeAction/Hole}/Misc.lean (89%)
 delete mode 100644 Std/Tactic/HoleCommand.lean

diff --git a/Std.lean b/Std.lean
index 799adacd61..bbc7213862 100644
--- a/Std.lean
+++ b/Std.lean
@@ -5,6 +5,11 @@ import Std.Classes.LawfulMonad
 import Std.Classes.Order
 import Std.Classes.RatCast
 import Std.Classes.SetNotation
+import Std.CodeAction
+import Std.CodeAction.Hole
+import Std.CodeAction.Hole.Attr
+import Std.CodeAction.Hole.Basic
+import Std.CodeAction.Hole.Misc
 import Std.Control.ForInStep
 import Std.Control.ForInStep.Basic
 import Std.Control.ForInStep.Lemmas
@@ -85,10 +90,6 @@ import Std.Tactic.Ext
 import Std.Tactic.Ext.Attr
 import Std.Tactic.GuardExpr
 import Std.Tactic.HaveI
-import Std.Tactic.HoleCommand
-import Std.Tactic.HoleCommand.Attr
-import Std.Tactic.HoleCommand.CodeAction
-import Std.Tactic.HoleCommand.Misc
 import Std.Tactic.Lint
 import Std.Tactic.Lint.Basic
 import Std.Tactic.Lint.Frontend
diff --git a/Std/CodeAction.lean b/Std/CodeAction.lean
new file mode 100644
index 0000000000..0e66a9cbac
--- /dev/null
+++ b/Std/CodeAction.lean
@@ -0,0 +1 @@
+import Std.CodeAction.Hole
diff --git a/Std/CodeAction/Hole.lean b/Std/CodeAction/Hole.lean
new file mode 100644
index 0000000000..88ed343391
--- /dev/null
+++ b/Std/CodeAction/Hole.lean
@@ -0,0 +1,3 @@
+import Std.CodeAction.Hole.Attr
+import Std.CodeAction.Hole.Basic
+import Std.CodeAction.Hole.Misc
diff --git a/Std/Tactic/HoleCommand/Attr.lean b/Std/CodeAction/Hole/Attr.lean
similarity index 56%
rename from Std/Tactic/HoleCommand/Attr.lean
rename to Std/CodeAction/Hole/Attr.lean
index 1ed9514941..21b31c2cdd 100644
--- a/Std/Tactic/HoleCommand/Attr.lean
+++ b/Std/CodeAction/Hole/Attr.lean
@@ -9,45 +9,43 @@ import Std.Util.TermUnsafe
 /-!
 # Initial setup for hole commands
 
-This declares an attribute `@[hole_command]` which collects code actions which will be called
+This declares an attribute `@[hole_code_action]` which collects code actions which will be called
 on each occurrence of a hole (`_`, `?_` or `sorry`).
 -/
-namespace Std.Tactic
+namespace Std.CodeAction
 
 open Lean Elab Server Lsp RequestM Snapshots
 
-/-- A hole command extension. -/
-abbrev HoleCommand :=
+/-- A hole code action extension. -/
+abbrev HoleCodeAction :=
   CodeActionParams → Snapshot →
   (ctx : ContextInfo) → (hole : TermInfo) → RequestM (Array LazyCodeAction)
 
-namespace HoleCommand
-
-/-- Read a `positivity` extension from a declaration of the right type. -/
-def mkHoleCommand (n : Name) : ImportM HoleCommand := do
+/-- 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 HoleCommand opts ``HoleCommand n
+  IO.ofExcept <| unsafe env.evalConstCheck HoleCodeAction opts ``HoleCodeAction n
 
-/-- An extension which collects all the hole commands. -/
-initialize holeCommandExt :
-    PersistentEnvExtension Name (Name × HoleCommand) (Array Name × Array HoleCommand) ←
+/-- 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 (← mkHoleCommand a))
+      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_command
-    descr := "Declare a new hole command, to appear in the code actions on ?_ and _"
+    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_command', must be global"
+        throwError "invalid attribute 'hole_code_action', must be global"
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
-      modifyEnv (holeCommandExt.addEntry · (decl, ← mkHoleCommand decl))
+      modifyEnv (holeCodeActionExt.addEntry · (decl, ← mkHoleCodeAction decl))
   }
diff --git a/Std/Tactic/HoleCommand/CodeAction.lean b/Std/CodeAction/Hole/Basic.lean
similarity index 59%
rename from Std/Tactic/HoleCommand/CodeAction.lean
rename to Std/CodeAction/Hole/Basic.lean
index 0c1c6218b6..ed1083524a 100644
--- a/Std/Tactic/HoleCommand/CodeAction.lean
+++ b/Std/CodeAction/Hole/Basic.lean
@@ -6,25 +6,26 @@ Authors: Mario Carneiro
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
 import Std.Lean.Name
-import Std.Tactic.HoleCommand.Attr
+import Std.CodeAction.Hole.Attr
 
 /-!
-# Initial setup for hole commands
+# Initial setup for hole code actions
 
-This declares a code action provider that calls all `@[hole_command]` definitions
+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.Tactic.HoleCommand.Attr` so that the server does not attempt
-to use this code action provider when browsing the `Std.Tactic.HoleCommand.Attr` file itself.)
+(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 Std.Tactic.HoleCommand
+namespace Std.CodeAction
 
 open Lean Elab.Term Server RequestM
 
 /--
-A code action which calls all `@[hole_command]` code actions on each hole (`?_`, `_`, or `sorry`).
+A code action which calls all `@[hole_code_action]` code actions on each hole
+(`?_`, `_`, or `sorry`).
 -/
-@[codeActionProvider] def holeCommandProvider : CodeActionProvider := fun params snap => do
+@[codeActionProvider] 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
@@ -36,4 +37,4 @@ A code action which calls all `@[hole_command]` code actions on each hole (`?_`,
     unless head ≤ endPos && startPos ≤ tail do return result
     result.push (ctx, info)
   let #[(ctx, info)] := holes | return #[]
-  (holeCommandExt.getState snap.env).2.concatMapM (· params snap ctx info)
+  (holeCodeActionExt.getState snap.env).2.concatMapM (· params snap ctx info)
diff --git a/Std/Tactic/HoleCommand/Misc.lean b/Std/CodeAction/Hole/Misc.lean
similarity index 89%
rename from Std/Tactic/HoleCommand/Misc.lean
rename to Std/CodeAction/Hole/Misc.lean
index 868dcba5c5..e4369a9931 100644
--- a/Std/Tactic/HoleCommand/Misc.lean
+++ b/Std/CodeAction/Hole/Misc.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Lean.Position
-import Std.Tactic.HoleCommand.CodeAction
+import Std.CodeAction.Hole.Basic
 
 /-!
-# Miscellaneous hole commands
+# Miscellaneous hole code actions
 
-This declares some basic hole commands, using the `@[hole_command]` API.
+This declares some basic hole code actions, using the `@[hole_code_action]` API.
 -/
-namespace Std.Tactic.HoleCommand
+namespace Std.CodeAction
 
 open Lean Server RequestM Meta
 
@@ -37,16 +37,14 @@ def holeKindToHoleString : (elaborator : Name) → (synthName : String) → Stri
   | _, _ => "_"
 
 /--
-Hole command used to fill in a structure's field when specifying an instance.
+Hole code action used to fill in a structure's field when specifying an instance.
 
 In the following:
-
 ```lean
 instance : Monad Id := _
 ```
 
-invoking the hole command "Generate a skeleton for the structure under construction." produces:
-
+invoking the hole code action "Generate a skeleton for the structure under construction." produces:
 ```lean
 instance : Monad Id := {
   map := _
@@ -59,7 +57,7 @@ instance : Monad Id := {
 }
 ```
 -/
-@[hole_command] partial def instanceStub : HoleCommand := fun params snap ctx info => do
+@[hole_code_action] partial def instanceStub : HoleCodeAction := fun params snap ctx info => do
   let some ty := info.expectedType? | return #[]
   let .const name _ := (← info.runMetaM ctx (whnf ty)).getAppFn | return #[]
   unless isStructure snap.env name do return #[]
@@ -110,8 +108,8 @@ where
       | none => fields.push field
 
 /--
-Invoking hole command "Generate a list of equations for a recursive definition" in the following:
-
+Invoking hole code action "Generate a list of equations for a recursive definition" in the
+following:
 ```lean
 def foo : Expr → Unit := _
 ```
@@ -135,7 +133,7 @@ def foo : Expr → Unit := fun
 ```
 
 -/
-@[hole_command] def eqnStub : HoleCommand := fun params snap ctx info => do
+@[hole_code_action] def eqnStub : HoleCodeAction := fun params snap ctx info => do
   let some ty := info.expectedType? | return #[]
   let .forallE _ dom .. ← info.runMetaM ctx (whnf ty) | return #[]
   let .const name _ := (← info.runMetaM ctx (whnf dom)).getAppFn | return #[]
diff --git a/Std/Tactic/HoleCommand.lean b/Std/Tactic/HoleCommand.lean
deleted file mode 100644
index 189cbcfd5d..0000000000
--- a/Std/Tactic/HoleCommand.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Std.Tactic.HoleCommand.Attr
-import Std.Tactic.HoleCommand.CodeAction
-import Std.Tactic.HoleCommand.Misc

From d3a3ec8dc4e05c6f918a95d73599ceecdf5711e3 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 9 May 2023 04:39:25 -0400
Subject: [PATCH 6/8] feat: tactic code actions framework

---
 Std.lean                         |   3 +
 Std/CodeAction/Tactic/Attr.lean  | 128 ++++++++++++++++++++++
 Std/CodeAction/Tactic/Basic.lean | 182 +++++++++++++++++++++++++++++++
 Std/CodeAction/Tactic/Misc.lean  |  49 +++++++++
 4 files changed, 362 insertions(+)
 create mode 100644 Std/CodeAction/Tactic/Attr.lean
 create mode 100644 Std/CodeAction/Tactic/Basic.lean
 create mode 100644 Std/CodeAction/Tactic/Misc.lean

diff --git a/Std.lean b/Std.lean
index bbc7213862..9183e1dbec 100644
--- a/Std.lean
+++ b/Std.lean
@@ -10,6 +10,9 @@ import Std.CodeAction.Hole
 import Std.CodeAction.Hole.Attr
 import Std.CodeAction.Hole.Basic
 import Std.CodeAction.Hole.Misc
+import Std.CodeAction.Tactic.Attr
+import Std.CodeAction.Tactic.Basic
+import Std.CodeAction.Tactic.Misc
 import Std.Control.ForInStep
 import Std.Control.ForInStep.Basic
 import Std.Control.ForInStep.Lemmas
diff --git a/Std/CodeAction/Tactic/Attr.lean b/Std/CodeAction/Tactic/Attr.lean
new file mode 100644
index 0000000000..789ee4a669
--- /dev/null
+++ b/Std/CodeAction/Tactic/Attr.lean
@@ -0,0 +1,128 @@
+/-
+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
+import Std.Util.TermUnsafe
+
+/-!
+# Initial setup for tactic commands
+
+This declares an attribute `@[tactic_code_action]` which collects code actions which will be called
+on each occurrence of a tactic (`_`, `?_` or `sorry`).
+-/
+namespace Std.CodeAction
+
+open Lean Elab Server Lsp RequestM Snapshots
+
+/-- A tactic code action extension. -/
+abbrev TacticCodeAction :=
+  CodeActionParams → Snapshot →
+  (ctx : ContextInfo) → (stack : Syntax.Stack) → (node : InfoTree) →
+  RequestM (Array LazyCodeAction)
+
+/-- A tactic code action extension. -/
+abbrev TacticSeqCodeAction :=
+  CodeActionParams → Snapshot →
+  (ctx : ContextInfo) → (i : Nat) → (stack : Syntax.Stack) →
+  (mctx : MetavarContext) → (goals : List MVarId) →
+  RequestM (Array LazyCodeAction)
+
+/-- Read a tactic code action from a declaration of the right type. -/
+def mkTacticCodeAction (n : Name) : ImportM TacticCodeAction := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck TacticCodeAction opts ``TacticCodeAction n
+
+/-- Read a tacticSeq code action from a declaration of the right type. -/
+def mkTacticSeqCodeAction (n : Name) : ImportM TacticSeqCodeAction := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck TacticSeqCodeAction opts ``TacticSeqCodeAction n
+
+/-- An entry in the tactic code actions extension, containing the attribute arguments. -/
+structure TacticCodeActionEntry where
+  /-- The declaration to tag -/
+  declName : Name
+  /-- The tactic kinds that this extension supports. If empty, it is called on tactic insertion
+  on the spaces between tactics, and if none it is called on all tactic kinds. -/
+  tacticKinds : Array Name
+  deriving Inhabited
+
+/-- The state of the tactic code actions extension. -/
+structure TacticCodeActions where
+  /-- The list of tactic code actions to apply on any tactic. -/
+  onAnyTactic : Array TacticCodeAction := {}
+  /-- The list of tactic code actions to apply when a particular tactic kind is highlighted. -/
+  onTactic : NameMap (Array TacticCodeAction) := {}
+  deriving Inhabited
+
+/-- Insert a tactic code action entry into the `TacticCodeActions` structure. -/
+def TacticCodeActions.insert (self : TacticCodeActions)
+    (tacticKinds : Array Name) (action : TacticCodeAction) : TacticCodeActions :=
+  if tacticKinds.isEmpty then
+    { self with onAnyTactic := self.onAnyTactic.push action }
+  else
+    { self with onTactic := tacticKinds.foldl (init := self.onTactic) fun m a =>
+        m.insert a ((m.findD a #[]).push action) }
+
+/-- An extension which collects all the tactic code actions. -/
+initialize tacticSeqCodeActionExt :
+    PersistentEnvExtension Name (Name × TacticSeqCodeAction)
+      (Array Name × Array TacticSeqCodeAction) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure (#[], #[])
+    addImportedFn := fun as => return (#[], ← as.foldlM (init := #[]) fun m as =>
+      as.foldlM (init := m) fun m a => return m.push (← mkTacticSeqCodeAction a))
+    addEntryFn := fun (s₁, s₂) (n₁, n₂) => (s₁.push n₁, s₂.push n₂)
+    exportEntriesFn := (·.1)
+  }
+
+/-- An extension which collects all the tactic code actions. -/
+initialize tacticCodeActionExt :
+    PersistentEnvExtension TacticCodeActionEntry (TacticCodeActionEntry × TacticCodeAction)
+      (Array TacticCodeActionEntry × TacticCodeActions) ←
+  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 (← mkTacticCodeAction name))
+    addEntryFn := fun (s₁, s₂) (e, n₂) => (s₁.push e, s₂.insert e.tacticKinds n₂)
+    exportEntriesFn := (·.1)
+  }
+
+/--
+This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
+
+* `@[tactic_code_action]`: This is a code action which applies to the spaces between tactics,
+  to suggest a new tactic to change the goal state.
+
+* `@[tactic_code_action kind]`: This is a code action which applies to applications of the tactic
+  `kind` (a tactic syntax kind), which can replace the tactic or insert things before or after it.
+
+* `@[tactic_code_action kind₁ kind₂]`: shorthand for
+  `@[tactic_code_action kind₁, tactic_code_action kind₂]`.
+-/
+syntax (name := tactic_code_action) "tactic_code_action" ("*" <|> ident*) : attr
+
+initialize
+  registerBuiltinAttribute {
+    name := `tactic_code_action
+    descr := "Declare a new tactic code action, to appear in the code actions on tactics"
+    applicationTime := .afterCompilation
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'tactic_code_action', must be global"
+      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      let _ := (decl, stx)
+      match stx with
+      | `(attr| tactic_code_action *) =>
+        modifyEnv (tacticCodeActionExt.addEntry · (⟨decl, #[]⟩, ← mkTacticCodeAction decl))
+      | `(attr| tactic_code_action $[$args]*) =>
+        if args.isEmpty then
+          modifyEnv (tacticSeqCodeActionExt.addEntry · (decl, ← mkTacticSeqCodeAction decl))
+        else
+          let args ← args.mapM fun arg => do
+            resolveGlobalConstNoOverloadWithInfo arg
+          modifyEnv (tacticCodeActionExt.addEntry · (⟨decl, args⟩, ← mkTacticCodeAction decl))
+      | _ => pure ()
+  }
diff --git a/Std/CodeAction/Tactic/Basic.lean b/Std/CodeAction/Tactic/Basic.lean
new file mode 100644
index 0000000000..69cb8674d6
--- /dev/null
+++ b/Std/CodeAction/Tactic/Basic.lean
@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Std.CodeAction.Tactic.Attr
+
+/-!
+# Initial setup for tactic code actions
+
+This declares a code action provider that calls `@[tactic_code_action]` definitions.
+
+(This is in a separate file from `Std.CodeAction.Tactic.Attr` so that the server does not attempt
+to use this code action provider when browsing the `Std.CodeAction.Tactic.Attr` file itself.)
+-/
+namespace Std.CodeAction
+
+open Lean Elab Server RequestM
+
+/--
+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) : Option Bool := do
+    guard <| (← stx.getPos? true) ≤ range.start
+    let .original (endPos := right) (trailing := trailing) .. := stx.getTailInfo | none
+    guard <| right.byteIdx + trailing.bsize ≥ range.stop.byteIdx
+    return 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) : 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
+      for i in [0:stx.getNumArgs] do
+        if let some _ := visit stx[i] then
+          if let some child ← go ((stx, i) :: stack) stx[i] then
+            if childRes.isSome then failure
+            childRes := child
+      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) (t : InfoTree)
+    (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
+    Option (ContextInfo × InfoTree) :=
+  go none t
+where
+  /-- `go ctx?` is like `findInfoTree?` but uses `ctx?` as the ambient `ContextInfo`. -/
+  go ctx?
+  | .context ctx t => go ctx t
+  | node@(.node i ts) => do
+    if let some ctx := ctx? then
+      let range ← i.stx.getRange? canonicalOnly
+      -- 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 := go (i.updateContext? ctx?) t then
+        return res
+    none
+  | _ => none
+
+/-- A code action which calls `@[tactic_code_action]` code actions. -/
+@[codeActionProvider] def tacticCodeActionProvider : 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
+  let pointerCol :=
+    if params.range.start.line == params.range.end.line then
+      max params.range.start.character params.range.end.character
+    else 0
+  let some result := findTactic?
+    (fun pos => (doc.meta.text.utf8PosToLspPos pos).character ≤ pointerCol)
+    ⟨startPos, endPos⟩ snap.stx | return #[]
+  let tgtTac := match result with
+    | .tactic (tac :: _)
+    | .tacticSeq _ _ (_ :: tac :: _) => tac.1
+    | _ => unreachable!
+  let tgtRange := tgtTac.getRange?.get!
+  have info := findInfoTree? tgtTac.getKind tgtRange snap.infoTree (canonicalOnly := true)
+    fun _ info => info matches .ofTacticInfo _
+  let some (ctx, node@(.node (.ofTacticInfo info) _)) := info | return #[]
+  let mut out := #[]
+  match result with
+  | .tactic stk@((tac, _) :: _) => do
+    let actions := (tacticCodeActionExt.getState snap.env).2
+    if let some arr := actions.onTactic.find? tac.getKind then
+      for act in arr do
+        out := out ++ (← act params snap ctx stk node)
+    for act in actions.onAnyTactic do
+      out := out ++ (← act params snap ctx stk node)
+  | .tacticSeq _ i stk@((seq, _) :: _) =>
+    let (ctx, mctx, goals) ← if 2*i < seq.getNumArgs then
+      pure (ctx, info.mctxAfter, info.goalsAfter)
+    else
+      let stx := seq[2*i]
+      let some stxRange := stx.getRange? | return #[]
+      let some (ctx, .node (.ofTacticInfo info') _) :=
+          findInfoTree? stx.getKind stxRange node fun _ info => (info matches .ofTacticInfo _)
+        | return #[]
+      pure (ctx, info'.mctxBefore, info'.goalsBefore)
+    for act in (tacticSeqCodeActionExt.getState snap.env).2 do
+      out := out ++ (← act params snap ctx i stk mctx goals)
+  | _ => unreachable!
+  pure out
diff --git a/Std/CodeAction/Tactic/Misc.lean b/Std/CodeAction/Tactic/Misc.lean
new file mode 100644
index 0000000000..a9039c4de6
--- /dev/null
+++ b/Std/CodeAction/Tactic/Misc.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Std.Lean.Position
+import Std.CodeAction.Tactic.Basic
+
+/-!
+# Miscellaneous tactic code actions
+
+This declares some basic tactic code actions, using the `@[tactic_code_action]` API.
+-/
+namespace Std.CodeAction
+
+open Lean Elab Server RequestM
+
+/-- The "Remove tactics after 'no goals'" code action deletes any tactics following a completed
+proof.
+```
+example : True := by
+  trivial
+  trivial -- <- remove this, proof is already done
+  rfl
+```
+is transformed to
+```
+example : True := by
+  trivial
+```
+-/
+@[tactic_code_action*]
+def removeAfterDoneAction : TacticCodeAction := fun params _ _ stk node => do
+  let .node (.ofTacticInfo info) _ := node | return #[]
+  unless info.goalsBefore.isEmpty do return #[]
+  let _ :: (seq, i) :: _ := stk | return #[]
+  let some stop := seq.getTailPos? | return #[]
+  let some prev := (seq.setArgs seq.getArgs[:i]).getTailPos? | return #[]
+  let doc ← readDoc
+  let eager := {
+    title := "Remove tactics after 'no goals'"
+    kind? := "quickfix"
+    isPreferred? := true
+    edit? := some <|.ofTextEdit params.textDocument.uri {
+      range := doc.meta.text.utf8PosToLspRange prev stop
+      newText := ""
+    }
+  }
+  pure #[{ eager }]

From e4b9a39002faf6b2b6f761a8a710df6efe6fd75b Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 10 May 2023 02:08:44 -0400
Subject: [PATCH 7/8] feat: induction auto-fill code action

---
 Std/CodeAction/Hole/Misc.lean    | 22 +++------
 Std/CodeAction/Tactic/Attr.lean  |  7 +--
 Std/CodeAction/Tactic/Basic.lean | 13 ++---
 Std/CodeAction/Tactic/Misc.lean  | 81 +++++++++++++++++++++++++++++++-
 Std/Lean/Position.lean           |  9 ++++
 5 files changed, 107 insertions(+), 25 deletions(-)

diff --git a/Std/CodeAction/Hole/Misc.lean b/Std/CodeAction/Hole/Misc.lean
index e4369a9931..0519f4a7de 100644
--- a/Std/CodeAction/Hole/Misc.lean
+++ b/Std/CodeAction/Hole/Misc.lean
@@ -21,15 +21,6 @@ def findStack? (root target : Syntax) : Option Syntax.Stack := do
   root.findStack? (·.getRange?.any (·.includes range))
     (fun s => s.getKind == target.getKind && s.getRange? == range)
 
-/--
-Return the indentation (number of leading spaces) of the line containing `pos`,
-and whether `pos` is the first non-whitespace character in the line.
--/
-def findIndentAndIsStart (s : String) (pos : String.Pos) : Nat × Bool :=
-  let start := findLineStart s pos
-  let body := s.findAux (· ≠ ' ') pos start
-  ((body - start).1, body == pos)
-
 /-- Constructs a hole with a kind matching the provided hole elaborator.  -/
 def holeKindToHoleString : (elaborator : Name) → (synthName : String) → String
   | ``Elab.Term.elabSyntheticHole, name => "?" ++ name
@@ -107,6 +98,12 @@ where
       | some substructName => collectFields env substructName fields
       | none => fields.push field
 
+/-- Returns the explicit arguments given a type. -/
+def getExplicitArgs : Expr → Array Name → Array Name
+  | .forallE n _ body bi, args =>
+    getExplicitArgs body <| if bi.isExplicit then args.push n else args
+  | _, args => args
+
 /--
 Invoking hole code action "Generate a list of equations for a recursive definition" in the
 following:
@@ -154,7 +151,7 @@ def foo : Expr → Unit := fun
         let some (.ctorInfo ci) := snap.env.find? ctor | panic! "bad inductive"
         let ctor := toString (ctor.updatePrefix .anonymous)
         str := str ++ indent ++ s!"| .{ctor}"
-        for arg in getArgs ci.type #[] do
+        for arg in getExplicitArgs ci.type #[] do
           str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
         str := str ++ s!" => {holeKindToHoleString info.elaborator ctor}"
       pure { eager with
@@ -164,8 +161,3 @@ def foo : Expr → Unit := fun
         }
       }
   }]
-where
-  /-- Returns the explicit arguments given a type. -/
-  getArgs : Expr → Array Name → Array Name
-  | .forallE n _ body bi, args => getArgs body <| if bi.isExplicit then args.push n else args
-  | _, args => args
diff --git a/Std/CodeAction/Tactic/Attr.lean b/Std/CodeAction/Tactic/Attr.lean
index 789ee4a669..8bfd0a11d7 100644
--- a/Std/CodeAction/Tactic/Attr.lean
+++ b/Std/CodeAction/Tactic/Attr.lean
@@ -25,8 +25,7 @@ abbrev TacticCodeAction :=
 /-- A tactic code action extension. -/
 abbrev TacticSeqCodeAction :=
   CodeActionParams → Snapshot →
-  (ctx : ContextInfo) → (i : Nat) → (stack : Syntax.Stack) →
-  (mctx : MetavarContext) → (goals : List MVarId) →
+  (ctx : ContextInfo) → (i : Nat) → (stack : Syntax.Stack) → (goals : List MVarId) →
   RequestM (Array LazyCodeAction)
 
 /-- Read a tactic code action from a declaration of the right type. -/
@@ -112,17 +111,19 @@ initialize
     add := fun decl stx kind => do
       unless kind == AttributeKind.global do
         throwError "invalid attribute 'tactic_code_action', must be global"
-      if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
       let _ := (decl, stx)
       match stx with
       | `(attr| tactic_code_action *) =>
+        if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
         modifyEnv (tacticCodeActionExt.addEntry · (⟨decl, #[]⟩, ← mkTacticCodeAction decl))
       | `(attr| tactic_code_action $[$args]*) =>
         if args.isEmpty then
+          if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
           modifyEnv (tacticSeqCodeActionExt.addEntry · (decl, ← mkTacticSeqCodeAction decl))
         else
           let args ← args.mapM fun arg => do
             resolveGlobalConstNoOverloadWithInfo arg
+          if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
           modifyEnv (tacticCodeActionExt.addEntry · (⟨decl, args⟩, ← mkTacticCodeAction decl))
       | _ => pure ()
   }
diff --git a/Std/CodeAction/Tactic/Basic.lean b/Std/CodeAction/Tactic/Basic.lean
index 69cb8674d6..8394e1c943 100644
--- a/Std/CodeAction/Tactic/Basic.lean
+++ b/Std/CodeAction/Tactic/Basic.lean
@@ -160,23 +160,24 @@ where
   let mut out := #[]
   match result with
   | .tactic stk@((tac, _) :: _) => do
+    let ctx := { ctx with mctx := info.mctxBefore }
     let actions := (tacticCodeActionExt.getState snap.env).2
     if let some arr := actions.onTactic.find? tac.getKind then
       for act in arr do
-        out := out ++ (← act params snap ctx stk node)
+        try out := out ++ (← act params snap ctx stk node) catch _ => pure ()
     for act in actions.onAnyTactic do
-      out := out ++ (← act params snap ctx stk node)
+      try out := out ++ (← act params snap ctx stk node) catch _ => pure ()
   | .tacticSeq _ i stk@((seq, _) :: _) =>
-    let (ctx, mctx, goals) ← if 2*i < seq.getNumArgs then
-      pure (ctx, info.mctxAfter, info.goalsAfter)
+    let (ctx, goals) ← if 2*i < seq.getNumArgs then
+      pure ({ ctx with mctx := info.mctxAfter }, info.goalsAfter)
     else
       let stx := seq[2*i]
       let some stxRange := stx.getRange? | return #[]
       let some (ctx, .node (.ofTacticInfo info') _) :=
           findInfoTree? stx.getKind stxRange node fun _ info => (info matches .ofTacticInfo _)
         | return #[]
-      pure (ctx, info'.mctxBefore, info'.goalsBefore)
+      pure ({ ctx with mctx := info'.mctxBefore }, info'.goalsBefore)
     for act in (tacticSeqCodeActionExt.getState snap.env).2 do
-      out := out ++ (← act params snap ctx i stk mctx goals)
+      try out := out ++ (← act params snap ctx i stk goals) catch _ => pure ()
   | _ => unreachable!
   pure out
diff --git a/Std/CodeAction/Tactic/Misc.lean b/Std/CodeAction/Tactic/Misc.lean
index a9039c4de6..e22ad604e6 100644
--- a/Std/CodeAction/Tactic/Misc.lean
+++ b/Std/CodeAction/Tactic/Misc.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Std.Lean.Name
 import Std.Lean.Position
 import Std.CodeAction.Tactic.Basic
 
@@ -13,7 +14,7 @@ This declares some basic tactic code actions, using the `@[tactic_code_action]`
 -/
 namespace Std.CodeAction
 
-open Lean Elab Server RequestM
+open Lean Meta Elab Server RequestM
 
 /-- The "Remove tactics after 'no goals'" code action deletes any tactics following a completed
 proof.
@@ -47,3 +48,81 @@ def removeAfterDoneAction : TacticCodeAction := fun params _ _ stk node => do
     }
   }
   pure #[{ eager }]
+
+/--
+Similar to `getElabInfo`, but returns the names of binders instead of just the numbers;
+intended for code actions which need to name the binders.
+-/
+def getElimNames (declName : Name) : MetaM (Array (Name × Array Name)) := do
+  let decl ← getConstInfo declName
+  forallTelescopeReducing decl.type fun xs type => do
+    let motive  := type.getAppFn
+    let targets := type.getAppArgs
+    let mut altsInfo := #[]
+    for i in [:xs.size] do
+      let x := xs[i]!
+      if x != motive && !targets.contains x then
+        let xDecl ← x.fvarId!.getDecl
+        if xDecl.binderInfo.isExplicit then
+          let args ← forallTelescopeReducing xDecl.type fun args _ => do
+            let lctx ← getLCtx
+            pure <| args.map fun fvar => (lctx.find? fvar.fvarId!).get!.userName
+          altsInfo := altsInfo.push (xDecl.userName, args)
+    pure altsInfo
+
+/--
+Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the
+following:
+```lean
+example (e : Nat) : Nat := by
+  induction e
+```
+produces:
+```lean
+example (e : Nat) : Nat := by
+  induction e with
+  | zero => done
+  | succ n n_ih => done
+```
+
+It also works for `cases`.
+-/
+@[tactic_code_action Parser.Tactic.cases Parser.Tactic.induction]
+def casesExpand : TacticCodeAction := fun params snap ctx _ node => do
+  let .node (.ofTacticInfo info) _ := node | return #[]
+  let (discr, induction) ← match info.stx with
+    | `(tactic| cases $[$_ :]? $e) => pure (e, false)
+    | `(tactic| induction $e $[generalizing $_*]?) => pure (e, true)
+    | _ => return #[]
+  let some (.ofTermInfo discrInfo) := node.findInfo? fun i =>
+    i.stx.getKind == discr.raw.getKind && i.stx.getRange? == discr.raw.getRange?
+    | return #[]
+  let .const name _ := (← discrInfo.runMetaM ctx (do whnf (← inferType discrInfo.expr))).getAppFn
+    | return #[]
+  let tacName := info.stx.getKind.updatePrefix .anonymous
+  let eager := {
+    title := s!"Generate an explicit pattern match for '{tacName}'."
+    kind? := "quickfix"
+  }
+  let doc ← readDoc
+  pure #[{
+    eager
+    lazy? := some do
+      let tacPos := info.stx.getPos?.get!
+      let endPos := doc.meta.text.utf8PosToLspPos info.stx.getTailPos?.get!
+      let mut str := " with"
+      let indent := "\n".pushn ' ' (findIndentAndIsStart doc.meta.text.source tacPos).1
+      let elimName := if induction then mkRecName name else mkCasesOnName name
+      for (name, args) in ← discrInfo.runMetaM ctx (getElimNames elimName) do
+        let mut ctor := toString name
+        if let some _ := (Parser.getTokenTable snap.env).find? ctor then
+          ctor := s!"{idBeginEscape}{ctor}{idEndEscape}"
+        str := str ++ indent ++ s!"| {ctor}"
+        for arg in args do
+          str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
+        str := str ++ s!" => done"
+      pure { eager with
+        edit? := some <|.ofTextEdit params.textDocument.uri
+          { range := ⟨endPos, endPos⟩, newText := str }
+      }
+  }]
diff --git a/Std/Lean/Position.lean b/Std/Lean/Position.lean
index 1bc4634d90..217f912410 100644
--- a/Std/Lean/Position.lean
+++ b/Std/Lean/Position.lean
@@ -18,3 +18,12 @@ def Lean.findLineStart (s : String) (pos : String.Pos) : String.Pos :=
   match s.revFindAux (· = '\n') pos with
   | none => 0
   | some n => ⟨n.byteIdx + 1⟩
+
+/--
+Return the indentation (number of leading spaces) of the line containing `pos`,
+and whether `pos` is the first non-whitespace character in the line.
+-/
+def Lean.findIndentAndIsStart (s : String) (pos : String.Pos) : Nat × Bool :=
+  let start := findLineStart s pos
+  let body := s.findAux (· ≠ ' ') pos start
+  ((body - start).1, body == pos)

From ff65288c5a0141c8eef97dc54f72e2e56d2382b1 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 10 May 2023 16:55:08 -0400
Subject: [PATCH 8/8] feat: use `sorry` instead of `done`, use `ih` name

---
 Std/CodeAction/Tactic/Misc.lean | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/Std/CodeAction/Tactic/Misc.lean b/Std/CodeAction/Tactic/Misc.lean
index e22ad604e6..b963afdf2d 100644
--- a/Std/CodeAction/Tactic/Misc.lean
+++ b/Std/CodeAction/Tactic/Misc.lean
@@ -74,15 +74,15 @@ def getElimNames (declName : Name) : MetaM (Array (Name × Array Name)) := do
 Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the
 following:
 ```lean
-example (e : Nat) : Nat := by
-  induction e
+example (x : Nat) : x = x := by
+  induction x
 ```
 produces:
 ```lean
-example (e : Nat) : Nat := by
-  induction e with
-  | zero => done
-  | succ n n_ih => done
+example (x : Nat) : x = x := by
+  induction x with
+  | zero => sorry
+  | succ n ih => sorry
 ```
 
 It also works for `cases`.
@@ -118,9 +118,15 @@ def casesExpand : TacticCodeAction := fun params snap ctx _ node => do
         if let some _ := (Parser.getTokenTable snap.env).find? ctor then
           ctor := s!"{idBeginEscape}{ctor}{idEndEscape}"
         str := str ++ indent ++ s!"| {ctor}"
+        -- replace n_ih with just ih if there is only one
+        let args := if induction &&
+          args.foldl (fun c n => if n.getString!.endsWith "_ih" then c+1 else c) 0 == 1
+        then
+          args.map (fun n => if n.getString!.endsWith "_ih" then `ih else n)
+        else args
         for arg in args do
           str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
-        str := str ++ s!" => done"
+        str := str ++ s!" => sorry"
       pure { eager with
         edit? := some <|.ofTextEdit params.textDocument.uri
           { range := ⟨endPos, endPos⟩, newText := str }