Lean highlight does not support -- line comment

[cireu]

I test the Lean 4 in Shiki at https://shiki.matsu.io/

And I found Shiki cannot render the -- comment of Lean correctly.

(See the different between /- test -/ and -- comment).

[cireu]

structure Point (α : Type u) where
  mk :: (x : α) (y : α)
  deriving Repr

/- test -/
#check Point       -- a Type
#check @Point.rec  -- the eliminator
#check @Point.mk   -- the constructor
#check @Point.x    -- a projection
#check @Point.y    -- a projection

#eval Point.x (Point.mk 10 20)
#eval Point.y (Point.mk 10 20)

It seems that Github can render this correct.

[slevithan]

textmate-grammars-themes (and by extension Shiki) gets the lean grammar from upstream here: https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json

I don't know if GitHub is using the same grammar file.

Does this work correctly if using the upstream grammar directly (rather than the cleaned up version from textmate-grammars-themes)?

• If yes, it could indeed be a problem with textmate-grammars-themes.
• But if not, the issue needs to be filed and fixed in the upstream grammar.
  • After a fix is committed there it will automatically be picked up here.