Missing goals in infoview when using `;`

Stream: general

[Eric Wieser]

mwe:

example (a b : ℕ) : a = a ∧ b = b :=
begin
  split,  -- two goals: `a = a`, `b = b`
  apply id,  -- one goal `a = a`
  refl; apply id, -- one goal `b = b`
  refl; apply id,
end

Comments show the goal state at the end of each line, after the comma. If a line contains a ;, then the goal view at the end of the previous line is truncated to show just one goal.

[Gabriel Ebner]

lean#201

[Eric Wieser]

Right, this is exactly the report in this comment: https://github.com/leanprover-community/lean/issues/201#issuecomment-654603146