From 0799e5c4e9d2aa8536bee5dbe91c9d11bab30874 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 15 Sep 2025 09:40:11 -0700 Subject: [PATCH] fix: make sure error ranges for `if` tactic are correct (#10392) This PR fixes an issue with the `if` tactic where errors were not placed at the correct source ranges. It also adds some error recovery to avoid additional errors about unsolved goals on the `if` token when the tactic has incomplete syntax. Closes #7972 --- src/Init/TacticsExtra.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean index 1ccbe8ff25..182a514a1d 100644 --- a/src/Init/TacticsExtra.lean +++ b/src/Init/TacticsExtra.lean @@ -24,14 +24,17 @@ private def expandIfThenElse pure (⟨holeOrTacticSeq⟩, #[]) else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then pure (← mkName, #[]) + else if tk.isMissing then + pure (← `(sorry), #[]) else let hole ← withFreshMacroScope mkName - let holeId := hole.raw[1] - let case ← (open TSyntax.Compat in `(tactic| - case $holeId:ident =>%$tk - -- annotate `then/else` with state after `case` - with_annotate_state $tk skip - $holeOrTacticSeq)) + let holeId : Ident := ⟨hole.raw[1]⟩ + let tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨holeOrTacticSeq⟩ + -- Use `missing` for ref to ensure that the source range is the same as `holeOrTacticSeq`'s. + let tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← MonadRef.withRef .missing `(tacticSeq| + with_annotate_state $tk skip + ($tacticSeq)) + let case ← withRef tk <| `(tactic| case $holeId:ident =>%$tk $tacticSeq:tacticSeq) pure (hole, #[case]) let (posHole, posCase) ← mkCase thenTk pos `(?pos) let (negHole, negCase) ← mkCase elseTk neg `(?neg)