diff --git a/src/html/html_page.ml b/src/html/html_page.ml
index da778f13ab..1b467faf5c 100644
--- a/src/html/html_page.ml
+++ b/src/html/html_page.ml
@@ -105,7 +105,194 @@ let page_creator ~config ~url ~uses_katex header breadcrumbs toc content =
             ]
           ();
         Html.script ~a:[ Html.a_src highlight_js_uri ] (Html.txt "");
-        Html.script (Html.txt "hljs.initHighlightingOnLoad();");
+        Html.script (Html.txt {tt|
+     /* Taken from https://github.com/highlightjs/highlight.js/issues/2889 */
+
+     var mergeHTMLPlugin = (function () {
+         'use strict';
+
+         var originalStream;
+
+         /**
+          * @param {string} value
+          * @returns {string}
+          */
+         function escapeHTML(value) {
+             return value
+                 .replace(/&/g, '&')
+                 .replace(/</g, '&lt;')
+                 .replace(/>/g, '&gt;')
+                 .replace(/"/g, '&quot;')
+                 .replace(/'/g, '&#x27;');
+         }
+
+         /* plugin itself */
+
+         /** @type {HLJSPlugin} */
+         const mergeHTMLPlugin = {
+             // preserve the original HTML token stream
+             "before:highlightElement": ({ el }) => {
+                 originalStream = nodeStream(el);
+             },
+             // merge it afterwards with the highlighted token stream
+             "after:highlightElement": ({ el, result, text }) => {
+                 if (!originalStream.length) return;
+
+                 const resultNode = document.createElement('div');
+                 resultNode.innerHTML = result.value;
+                 result.value = mergeStreams(originalStream, nodeStream(resultNode), text);
+                 el.innerHTML = result.value;
+             }
+         };
+
+         /* Stream merging support functions */
+
+         /**
+          * @typedef Event
+          * @property {'start'|'stop'} event
+          * @property {number} offset
+          * @property {Node} node
+          */
+
+         /**
+          * @param {Node} node
+          */
+         function tag(node) {
+             return node.nodeName.toLowerCase();
+         }
+
+         /**
+          * @param {Node} node
+          */
+         function nodeStream(node) {
+             /** @type Event[] */
+             const result = [];
+             (function _nodeStream(node, offset) {
+                 for (let child = node.firstChild; child; child = child.nextSibling) {
+                     if (child.nodeType === 3) {
+                         offset += child.nodeValue.length;
+                     } else if (child.nodeType === 1) {
+                         result.push({
+                             event: 'start',
+                             offset: offset,
+                             node: child
+                         });
+                         offset = _nodeStream(child, offset);
+                         // Prevent void elements from having an end tag that would actually
+                         // double them in the output. There are more void elements in HTML
+                         // but we list only those realistically expected in code display.
+                         if (!tag(child).match(/br|hr|img|input/)) {
+                             result.push({
+                                 event: 'stop',
+                                 offset: offset,
+                                 node: child
+                             });
+                         }
+                     }
+                 }
+                 return offset;
+             })(node, 0);
+             return result;
+         }
+
+         /**
+          * @param {any} original - the original stream
+          * @param {any} highlighted - stream of the highlighted source
+          * @param {string} value - the original source itself
+          */
+         function mergeStreams(original, highlighted, value) {
+             let processed = 0;
+             let result = '';
+             const nodeStack = [];
+
+             function selectStream() {
+                 if (!original.length || !highlighted.length) {
+                     return original.length ? original : highlighted;
+                 }
+                 if (original[0].offset !== highlighted[0].offset) {
+                     return (original[0].offset < highlighted[0].offset) ? original : highlighted;
+                 }
+
+                 /*
+                    To avoid starting the stream just before it should stop the order is
+                    ensured that original always starts first and closes last:
+
+                    if (event1 == 'start' && event2 == 'start')
+                    return original;
+                    if (event1 == 'start' && event2 == 'stop')
+                    return highlighted;
+                    if (event1 == 'stop' && event2 == 'start')
+                    return original;
+                    if (event1 == 'stop' && event2 == 'stop')
+                    return highlighted;
+
+                    ... which is collapsed to:
+                  */
+                 return highlighted[0].event === 'start' ? original : highlighted;
+             }
+
+             /**
+              * @param {Node} node
+              */
+             function open(node) {
+                 /** @param {Attr} attr */
+                 function attributeString(attr) {
+                     return ' ' + attr.nodeName + '="' + escapeHTML(attr.value) + '"';
+                 }
+                 // @ts-ignore
+                 result += '<' + tag(node) + [].map.call(node.attributes, attributeString).join('') + '>';
+             }
+
+             /**
+              * @param {Node} node
+              */
+             function close(node) {
+                 result += '</' + tag(node) + '>';
+             }
+
+             /**
+              * @param {Event} event
+              */
+             function render(event) {
+                 (event.event === 'start' ? open : close)(event.node);
+             }
+
+             while (original.length || highlighted.length) {
+                 let stream = selectStream();
+                 result += escapeHTML(value.substring(processed, stream[0].offset));
+                 processed = stream[0].offset;
+                 if (stream === original) {
+                     /*
+                        On any opening or closing tag of the original markup we first close
+                        the entire highlighted node stack, then render the original tag along
+                        with all the following original tags at the same offset and then
+                        reopen all the tags on the highlighted stack.
+                      */
+                     nodeStack.reverse().forEach(close);
+                     do {
+                         render(stream.splice(0, 1)[0]);
+                         stream = selectStream();
+                     } while (stream === original && stream.length && stream[0].offset === processed);
+                     nodeStack.reverse().forEach(open);
+                 } else {
+                     if (stream[0].event === 'start') {
+                         nodeStack.push(stream[0].node);
+                     } else {
+                         nodeStack.pop();
+                     }
+                     render(stream.splice(0, 1)[0]);
+                 }
+             }
+             return result + escapeHTML(value.substr(processed));
+         }
+
+         return mergeHTMLPlugin;
+
+     }());
+
+     hljs.addPlugin(mergeHTMLPlugin);
+
+hljs.initHighlightingOnLoad();|tt});
       ]
     in
     let meta_elements =