Lean block comment not correct

[jasoneveleth]

First of all, thank you for the plugin.

I noticed that block comments weren't being highlighted right. The code following the block comment is greyed out.

import .love01_definitions_and_statements_demo

/- test -/

set_option pp.beta true
set_option pp.generalized_field_notation false

I was able to fix this by changing lines 78 and 79, into this:

syn region      leanBlockComment start="/-" end="-/" contains=@markdown,@Spell
syn match       leanBlockComment     "--.*" contains=@Spell
hi link leanBlockComment leanComment

Removing the leanBlockComment in the contains field, and changing the sun match to leanBlockComment, and finally linking the block comment to a normal comment.

[gebner]

Hi Jason!

This plugin is no longer maintained. If you are by any chance using neovim, then please check out our new lean.nvim plugin, which has server support to show diagnostics, go-to-definition, etc. (and soon also interactive widgets).

The lean.nvim syntax file works correctly with your example. I could update the syntax file in this repo with the one from lean.nvim, but there won't be any new development here.