From d9617ad0ecc690d9c2a8b84775d228adadcbf2a9 Mon Sep 17 00:00:00 2001 From: Paul-Elliot Date: Wed, 23 Aug 2023 18:20:24 +0200 Subject: [PATCH] register a plugin to use html markup in highlighted blocks Plugin is taken from https://github.com/highlightjs/highlight.js/issues/2889 Signed-off-by: Paul-Elliot --- src/html/html_page.ml | 189 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 188 insertions(+), 1 deletion(-) 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, '>') + .replace(/"/g, '"') + .replace(/'/g, '''); + } + + /* 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 += ''; + } + + /** + * @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 =