bad error message with unclosed comment

Stream: lean4

[Floris van Doorn]

If you have an unclosed comment in your file, the error messages are not great:

example (n : Nat) : Nat → Nat :=
  Nat.add n -- type mismatch
/-

or

example (n : Nat) : Nat → Nat :=
  Nat.add n -- type mismatch
#exit
/-

Note:

example (n : Nat) : Nat → Nat :=
  Nat.add n -- fine

[Floris van Doorn]

(there is also an unterminated comment error in the first two examples)