Support syntax highlighting for Lean in Markdown code blocks

[hansonchar]

When generating documentation with markdown in doc-gen4, code blocks tagged as lean or lean4 (e.g., ```lean or ```lean4) currently do not support syntax highlighting. Are there any plans to add support for Lean syntax highlighting in markdown code blocks?

[eric-wieser]

Currently no fenced code-block highlighting is supported, I think.

[acmepjz]

I've checked the md4c source code, at least it will put the XXX in ```XXX to HTML. So maybe we should try to load a javascript for syntax highlighting?