372f344155
This PR resolves the following issues related to goal state display: 1. In a new line after a `case` tactic with a completed proof, the state of the proof in the `case` would be displayed, not the proof state after the `case` 1. In the range of `next =>` / `case' ... =>`, the state of the proof in the corresponding case would not be displayed, whereas this is true for `case` 1. In the `suffices ... by` tactic, the tactic state of the `by` block was not displayed after the `by` and before the first tactic The incorrect goal state after `case` was caused by `evalCase` adding a `TacticInfo` with the full block proof state for the full range of the `case` block that the goal state selection has no means of distinguishing from the `TacticInfo` with the same range that contains the state after the whole `case` block. Narrowing the range of this `TacticInfo` to `case ... =>` fixed this issue. The lack of a case proof state on `next =>` was caused by the `case` syntax that `next` expands to receiving noncanonical synthetic `SourceInfo`, which is usually ignored by the language server. Adding a token antiquotation for `next` fixed this issue. The lack of a case proof state on `case' ... =>` was caused by `evalCase'` not adding a `TacticInfo` with the full block state to the range of `case' ... =>`. Adding this `TacticInfo` fixed this issue. The tactic state of the block not being displayed after the `by` was caused by the macro expansion of `suffices` to `have` not transferring the trailing whitespace of the `by`. Ensuring that this trailing whitespace information is transferred fixed this issue. Fixes #2881. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||