Bug: 'unterminated comment' when you have `/-` in a docstrin

Stream: lean4 dev

[Alex Keizer]

I've been breaking my head over an 'unterminated comment' error at the very end of a file. Turns out, I had +/- in a docstring somewhere, as in the following MWE:

/-- `x +/- y` -/
def test : String := "foo"

-- We get `unterminated comment` at the *end* of the file, even if we introduce other definitions after `test`

(confirmed on nightly-2024-08-11)

The workaround is easy, but this seems like a bug. At the very least, the error should be located at the actual comment that it believes to be unterminated, but I think having /- inside a docstring should not be seen as starting a nested comment.

Also, VSCode highlights the docstring in the MWE as expected, making it appear properly terminated

EDIT: Cross-posted to https://github.com/leanprover/lean4/issues/5005