RFC: show robust tactic state

Proposal

The goal of this RFC is to have the tactic state not change too much while typing.
This is a complaint I have heard more than once from beginners: "The goal state is jumping around too much". You can pause the goal state, but this is a bit of an inconvenient workaround.

Examples with current behavior:

-- in each example place the pointer right before the `--`
example : True ∧ False ∧ True := by
  simp only [false_and]
  ex -- <no tactic state> / errors: unknown tactic & unsolved goals

example : True ∧ False ∧ True := by
  simp only [false_and]
  exact -- Tactic state: No goals / error: unexpected token 

example : True ∧ False ∧ True := by
  simp only [false_and]
  exact true -- Shows the correct tactic state / error: type mismatch

example : True ∧ False ∧ True := by
  simp only [false_and]
  exact true_ -- Tactic state: No goals / error: unknown identifier

example : True ∧ False ∧ True := by
  simp only [false_and]
  apply true_ -- Shows the correct tactic state / error: unknown identifier

Desired behavior: All examples should show the tactic state that is shown in examples 3 and 5.

• User Experience: This should be a improvement for all users.

• Beneficiaries: Especially new users, slow typers. But can benefit anyone that tries to apply a tactic, see that it errors, and wants to easily see the previous tactic state.

• Maintainability: Should not significantly impact maintainability.

Implementation speculation: Hopefully the first example can be fixed by having a rule that any non-existent tactic still shows the tactic state from the start of the line. And maybe example 2 can be fixed by having a parse error do the same?
Example 4 can probably be fixed in the implementation of exact (it works with apply, see example 5).

Community Feedback

Zulip, 2

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reproducing the five examples in the issue and compare the tactic states while editing. Read the behavior around parsing, unknown tactics, and the exact and apply implementations, along with the linked community discussions. Done means unfinished lines consistently preserve the prior useful tactic state without hiding relevant errors.