fix: report goals in induction with parse error

src/Lean/Elab/Tactic/Induction.lean

@@ -264,7 +264,6 @@ def reorderAlts (alts : Array Alt) (altsSyntax : Array Syntax) : Array Alt := Id
 def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altsSyntax : Array Syntax)
     (initialInfo : Info)
     (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do
-  checkAltNames alts altsSyntax
   let hasAlts := altsSyntax.size > 0
   if hasAlts then
     -- default to initial state outside of alts
@@ -276,6 +275,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (alts
   else go
 where
   go := do
+    checkAltNames alts altsSyntax
     let alts := reorderAlts alts altsSyntax
     let hasAlts := altsSyntax.size > 0
     let mut usedWildcard := false

tests/lean/interactive/plainGoal.lean

@@ -134,3 +134,16 @@ example : True ∧ False := by
   · --
  --^ $/lean/plainGoal
   --^ $/lean/plainGoal
+
+section
+
+example : True := by induction 1 with
+                                --^ $/lean/plainGoal
+
+example : True := by induction 1 with |
+                                --^ $/lean/plainGoal
+
+example : True := by induction 1 with done
+                                --^ $/lean/plainGoal
+
+end

tests/lean/interactive/plainGoal.lean.expected.out

@@ -170,3 +170,12 @@ null
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 133, "character": 4}}
 {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 139, "character": 34}}
+{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 142, "character": 34}}
+{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 145, "character": 34}}
+{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}