Add markdown comment syntax highlighting

[gebner]

The important ones are # headlines, *emphasis*, and `inline code`.

[Julian]

Do you recall any examples where the builtin syn include failed?

I've noticed there's a main_syntax variable we should have been setting before including the markdown syntax. If there still are issues, hopefully I'll notice them from some use before sending a PR re-adding, but for now:

diff --git a/syntax/lean.vim b/syntax/lean.vim
index 3c87fde..7ebae61 100644
--- a/syntax/lean.vim
+++ b/syntax/lean.vim
@@ -75,9 +75,10 @@ syn match leanNumber '\<\d\d*\.\d*\>'
 
 syn match leanNameLiteral '``*[^ \[()\]}][^ ()\[\]{}]*'
 
-" syn include     @markdown       syntax/markdown.vim
+let main_syntax = 'lean'
+syn include     @markdown       syntax/markdown.vim
 syn region      leanBlockComment start="/-" end="-/" contains=@markdown,@Spell,leanBlockComment
-syn match       leanComment     "--.*" contains=@Spell
+syn match       leanComment     "--.*" contains=@markdown,@Spell
 " fix up some highlighting links for markdown
 hi! link markdownCodeBlock Comment
 hi! link markdownError Comment
diff --git a/syntax/lean3.vim b/syntax/lean3.vim
index cbcce85..fe2f081 100644
--- a/syntax/lean3.vim
+++ b/syntax/lean3.vim
@@ -69,9 +69,10 @@ syn match leanNumber '\<\d\d*\.\d*\>'
 
 syn match leanNameLiteral '``*[^ \[()\]}][^ ()\[\]{}]*'
 
-" syn include     @markdown       syntax/markdown.vim
+let main_syntax = 'lean'
+syn include     @markdown       syntax/markdown.vim
 syn region      leanBlockComment start="/-" end="-/" contains=@markdown,@Spell,leanBlockComment
-syn match       leanComment     "--.*" contains=@Spell
+syn match       leanComment     "--.*" contains=@markdown,@Spell
 " fix up some highlighting links for markdown
 hi! link markdownCodeBlock Comment
 hi! link markdownError Comment

looks OK at first glance. Let me know if you recall anything specific I can look at to see if it's still syntax-broken.

[gebner]

Two examples where the markdown highlighting continues after comment ends:

/-!
# Headlines -/

/-!
    indented text -/

Looking through lean files in core and mathlib (and the Lean 4 versions) is a good idea.

[gebner]

Another common instance of the issue is commented-out code:

-- #eval `test

[Julian]

Yeah thanks, those were helpful (in the sense they showed that setting main_syntax didn't fix anything). I gave up again for now, this ticket was just distracting me when trying to read some long prose in a file and was annoyed it wasn't highlighted.