5d54b0b13f
This PR fixes a bug introduced in #7830 where if the cursor is at the indicated position ```lean example (as bs : List Nat) : (as.append bs).length = as.length + bs.length := by induction as with | nil => -- cursor | cons b bs ih => ``` then the Infoview would show "no goals" rather than the `nil` goal. The PR also fixes a separate bug where placing the cursor on the next line after the `induction`/`cases` tactics like in ```lean induction as with | nil => sorry | cons b bs ih => sorry I -- < cursor ``` would report the original goal in the goal list. Furthermore, there are numerous improvements to error recovery (including `allGoals`-type logic for pre-tactics) and the visible tactic states when there are errors. Adds `Tactic.throwOrLogErrorAt`/`Tactic.throwOrLogError` for throwing or logging errors depending on the recovery state.
9 lines
437 B
Text
9 lines
437 B
Text
{"textDocument": {"uri": "file:///tacticInduction.lean"},
|
|
"position": {"line": 9, "character": 10}}
|
|
{"rendered":
|
|
"```lean\ncase nil\nbs : List Nat\n⊢ ([].append bs).length = [].length + bs.length\n```",
|
|
"goals":
|
|
["case nil\nbs : List Nat\n⊢ ([].append bs).length = [].length + bs.length"]}
|
|
{"textDocument": {"uri": "file:///tacticInduction.lean"},
|
|
"position": {"line": 17, "character": 2}}
|
|
{"rendered": "no goals", "goals": []}
|