Figure out how to use newer highlightjs

[ehuss]

highlightjs 11 removed a feature called "HTML merging". This is a feature we are depending on to handle "boring" lines, which get wrapped with <span class="boring">. HLJS 11 now completely strips HTML out of a code block.

There is discussion at https://github.com/highlightjs/highlight.js/issues/2889 about writing a plugin to add this functionality back in, but I do not understand the plugin API well enough to write that (the current example there does not work).

Either we'll need to figure out how to get that working, or we'll need to find a new highlighting engine. #1494 is a potential route, though I am concerned about the significant performance loss.

[notriddle]

#1652 seems to perform a lot better than the earlier syntect benchmarks.

[sanmai-NL]

I have good experiences with Prism.js. Lightweight and very functional.

[ISSOtm]

I wanted to start working on this, but I don't want the effort to be wasted in case #1652 is merged instead. Should I go ahead regardless?

[joshgoebel]

What is a boring line? How does one know which lines are boring Before the highlighting has happened?