Comment bug

Stream: lean4

[Patrick Massot]

I'm sure I already reported this a long time ago, but there is still a bug when writing comments at the end of a file. This is very distracting when writing lecture material where I first write comments and then Lean code. Note the bug disappear when one reload the file.
comment_bug.gif

[Patrick Massot]

The above screencast was recorded a couple of seconds after typing lake +4.0.0 new pr.

[James Gallicchio]

I suspect it's related to how /- <EOF> gives that error message. if you paste in a comment at the end of the file, the error doesn't happen, right?

[Marc Huisinga]

Corresponding issue: lean4#1329

[Patrick Massot]

So indeed I reported it before.

[Julian Berman]

That doesn't reproduce in neovim at least

[Julian Berman]

(Just mentioning it in case it helps decide where to look)

[Julian Berman]

Actually here I can't reproduce that in VSCode either

[Julian Berman]

(Sorry for the quadruple post) -- but actually I can, but it depends on what sequence of letters you type to get the comment and how fast you type them?? Recording:

output.gif

(the gif encoding is actually messing with the "real life" typing speed there I see)

For further clarity, I can indeed reproduce in neovim if I match the order that one gets in VSCode -- which partially has to do with having autopair a default in VSCode (so you get /--/ immediately) whereas I don't have that enabled in neovim, and it seems harder to get this behavior with it off. But if I manually type /--/ in neovim and then "fill in" the middle, I get the same behavior.