Syntax highlighting bug makes everything blue

Stream: Editors & UIs

[Snir Broshi]

This bug might be VSCode only but I'm not sure. It doesn't seem to affect Zulip but I've seen mentions of the same syntax highlighting config being shared across multiple tools.

-- **a*a**a*

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

theorem factorial_zero : factorial 0 = 1 := rfl

image.png

As for the VSCode extension, I think this makes the line comment go into markdown mode, and then this handles the double-asterisks making everything bold.
But I'm not sure how it's able to leak outside the comment when the former specifies "end": "$".

Is this known? Does it replicate in Neovim/Emacs/Highlight.js/etc?

[Castedo Ellerman]

Snir Broshi said:

Does it replicate in Neovim/Emacs/Highlight.js/etc?

In VSCodium I see a similar strange effect triggered by that markdown comment (but with green text).

I see no such effect with Neovim and Vim.

[Marc Huisinga]

We want to get rid of the Markdown TextMate grammar integration eventually and replace it with proper semantic highlighting for Markdown in the language server. There are unfortunately many bugs of this nature in the TextMate grammar.