Mardown highlighting in comments consumes closing `-/`

[eric-wieser]

These aren't highlighted correctly:

1. /- Oh `-/` no -/
   #check 1
   

   The no -/ is not actually part of the comment.

2. /- [foo]: -/
   #check 1
   

   The #check should not be a comment.

[gebner]

Yeah, I am well aware that this can happen. I've been fixing them whenever they become an issue. Unfortunately it seems to be impossible to tell vscode to stop the markdown highlighting when it sees a -/, the markdown grammar needs to cooperate here and stop itself...

In general, I didn't prioritize invalid markdown syntax, because you should usually avoid it. See also https://github.com/leanprover-community/vscode-lean4/issues/10#issuecomment-796860331

[eric-wieser]

Perhaps I should have made my intention clear in opening this - I'm not after a fix, I figured it was just worth recording the bug in case someone else cares enough to fix it.

[eric-wieser]

IIRC, sublime text ended up augmenting their TextMate grammar handling to make this type of "just kill the inner parser if you find a -/" action possible. Perhaps vscode will eventually go the same way.