show robust tactic state while typing

Stream: lean4

[Floris van Doorn]

Ideally the tactic state doesn't 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.

If you agree, please upvote lean4#4181.