IIUC currently Block.toHtml renders .code blocks using only a <pre> container:
|
| .code content => pure #[{{ <pre> {{ content }} </pre>}}] |
This breaks client-side highlighters like Highlight.js and some CSS themes which expect the standard structrue. I think it would be great to reuse some existing highlighters as a catch-all highlighting on the top of define_lexed_text defined languages.
IIUC currently
Block.toHtmlrenders.codeblocks using only a<pre>container:verso/src/verso/Verso/Doc/Html.lean
Line 172 in 1e49d3d
This breaks client-side highlighters like Highlight.js and some CSS themes which expect the standard structrue. I think it would be great to reuse some existing highlighters as a catch-all highlighting on the top of
define_lexed_textdefined languages.