Syntax-highlight comments in verso code

[eric-wieser]

It would be great if a dedicate span tag was placed around -- and /- comments within a lean code snippet.

In https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html, I hacked around this with

            .hl.lean {
                color: #c92786
            }

            .hl.lean > * {
                color: black
            }

This might also align with future work to exploring rendering markdown and latex inside comments.

[david-christiansen]

This would absolutely be useful.

How would this structure work:

-- foo

becomes something along the lines of

<span class="comment line"><span class="delimiter">--</span> foo</span>

and

/- stuff /- nested -/
 -/

becomes

<span class="comment block"><span class="delimiter">/-</span> stuff /- nested -/
 <span class="delimiter">-/</span></span>

?

Also, it seems like it could be good to be able to parameterize the highlighting routines with a "comment handler" that transforms comments into something else. This would unlock Verso-enabled literate Lean, and many other interesting use cases, and might be nicer than doing it in post-processing (e.g., the source code info trees could be available in the handlers). Any thoughts on how to make it useful for you too?