feat: annotate match tactic alternatives with expected state

src/Lean/Elab/Tactic/Match.lean

@@ -15,6 +15,7 @@ structure AuxMatchTermState where
   nextIdx : Nat := 1
   «cases» : Array Syntax := #[]
 
+open Parser.Tactic in
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
   let matchAlts := matchTac[5]
   let alts      := matchAlts[0].getArgs
@@ -33,7 +34,11 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
     else withFreshMacroScope do
       let newHole ← `(?rhs)
       let newHoleId := newHole[1]
-      let newCase ← `(tactic| case $newHoleId =>%$(alt[2]) ($holeOrTacticSeq:tacticSeq) )
+      let newCase ← `(tactic|
+        case $newHoleId =>%$(alt[2])
+          -- annotate `| ... =>` with state after `case`
+          with_annotate_state $(mkNullNode #[alt[0], alt[2]]) skip
+          $holeOrTacticSeq)
       modify fun s => { s with cases := s.cases.push newCase }
       pure <| alt.setArg 3 newHole
   let result  := matchTac.setKind ``Parser.Term.«match»

tests/lean/interactive/infoIssues.lean

@@ -25,6 +25,6 @@ example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
                                  --v $/lean/plainGoal
   | y+1 => repeat rw [Nat.zero_add]
        --^ $/lean/plainGoal
-       -- Bad: get the `match` tactic initial state here.
+       -- Good: we get the succ state here
 --^ $/lean/plainGoal
 -- Good:  ... |- p

tests/lean/interactive/infoIssues.lean.expected.out

@@ -32,10 +32,8 @@
 {"textDocument": {"uri": "file://infoIssues.lean"},
  "position": {"line": 25, "character": 9}}
 {"rendered":
- "```lean\ncase left\np : Prop\nx : Nat\n⊢ x = 0 + (0 + (0 + x))\n```\n---\n```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```",
- "goals":
- ["case left\np : Prop\nx : Nat\n⊢ x = 0 + (0 + (0 + x))",
-  "case right\np : Prop\nx : Nat\n⊢ p"]}
+ "```lean\np : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (0 + (y + 1)))\n```",
+ "goals": ["p : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (0 + (y + 1)))"]}
 {"textDocument": {"uri": "file://infoIssues.lean"},
  "position": {"line": 27, "character": 2}}
 {"rendered": "```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```",