chore:

Author: leodemoura

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -27,14 +27,23 @@ import Lean.Elab.Tactic.Grind.Filter
 import Lean.Elab.Tactic.Grind.ShowState
 namespace Lean.Elab.Tactic.Grind
 
+def showStateAt (ref : Syntax) (filter : Filter) : GrindTacticM Unit := do
+  if let goalBefore :: _ := (← getGoals) then
+    withRef ref <| goalBefore.withContext <| showState filter (isSilent := true)
+  else
+    logAt ref (severity := .information) (isSilent := true) "no grind state"
+
 def evalSepTactics (stx : Syntax) : GrindTacticM Unit := do
   for arg in stx.getArgs, i in *...stx.getArgs.size do
     if i % 2 == 0 then
-      let `(Parser.Tactic.Grind.grindStep| $tac:grind $[| $[$filter??]?]?) := arg | throwUnsupportedSyntax
-      evalGrindTactic tac
-      if let some filter? := filter?? then
-        if let goal :: _ ← getGoals then
-          withRef stx <| goal.withContext <| showState filter? (silent := true)
+      match arg with
+      | `(Parser.Tactic.Grind.grindStep| $tac:grind) => evalGrindTactic tac
+      | `(Parser.Tactic.Grind.grindStep| $tac:grind | $[$filter?]?) =>
+        let filter ← elabFilter filter?
+        showStateAt arg filter
+        evalGrindTactic tac
+        showStateAt arg[1] filter
+      | _ => throwUnsupportedSyntax
     else
       saveTacticInfoForToken arg
 

src/Lean/Elab/Tactic/Grind/ShowState.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
-import Lean.Elab.Tactic.Grind.Filter
+public import Lean.Elab.Tactic.Grind.Filter
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.Split
@@ -92,18 +92,18 @@ def ppEqcs? (filter : Filter) (collapsed := false) : GrindTacticM (Option Messag
 def pushIfSome (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData :=
   if let some msg := msg? then msgs.push msg else msgs
 
-public def showState (filter? : Option (TSyntax `grind_filter)) (silent := false) : GrindTacticM Unit := do
-  let filter ← elabFilter filter?
+public def showState (filter : Filter) (isSilent := false) : GrindTacticM Unit := do
   let msgs := #[]
   let msgs := pushIfSome msgs (← ppAsserted? filter (collapsed := true))
   let msgs := pushIfSome msgs (← ppProps? filter true (collapsed := false))
   let msgs := pushIfSome msgs (← ppProps? filter false (collapsed := false))
   let msgs := pushIfSome msgs (← ppEqcs? filter (collapsed := false))
-  logAt (← getRef) (severity := .information) (isSilent := silent) <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs
+  logAt (← getRef) (severity := .information) (isSilent := isSilent) <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs
 
 @[builtin_grind_tactic Parser.Tactic.Grind.showState] def evalShowState : GrindTactic := fun stx => withMainContext do
   let `(grind| show_state $[$filter?]?) := stx | throwUnsupportedSyntax
-  showState filter?
+  let filter ← elabFilter filter?
+  showState filter
 
 @[builtin_grind_tactic showCases] def evalShowCases : GrindTactic := fun stx => withMainContext do
   let `(grind| show_cases $[$filter?]?) := stx | throwUnsupportedSyntax

tests/lean/run/grind_interactive.lean

@@ -401,7 +401,7 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind =>
-    instantiate Array.getElem_set
+    instantiate Array.getElem_set | gen > 0
     instantiate Array.getElem_set
 
 example (as bs cs : Array α) (v₁ v₂ : α)