☰

Boost.org - Source Highlight

Add code highlight to boost.org pages.

  1. // ==UserScript==
  2. // @name        Boost.org - Source Highlight
  3. // @namespace   uk.jixun
  4. // @match       https://www.boost.org/doc/*
  5. // @grant       none
  6. // @version     1.0
  7. // @author      Jixun
  8. // @description Add code highlight to boost.org pages.
  9. // @run-at      document-start
  10. // @license     apache-2.0
  11. // ==/UserScript==
  12.  
  13. function main() {
  14.   const codeBlocks = Array.from(document.querySelectorAll('pre'));
  15.   if (codeBlocks.length === 0) return;
  16.  
  17.   const stylesheet = document.createElement('link');
  18.   Object.assign(stylesheet, {
  19.     rel: 'stylesheet',
  20.     href: 'https://cdn.jsdelivr.net/gh/highlightjs/cdn-release@11.5.1/build/styles/default.min.css',
  21.   });
  22.   document.head.appendChild(stylesheet);
  23.  
  24.   const hljsScript = document.createElement('script');
  25.   Object.assign(hljsScript, {
  26.     src: 'https://cdn.jsdelivr.net/gh/highlightjs/cdn-release@11.5.1/build/highlight.min.js',
  27.     onload: () => {
  28.       hljs.configure({
  29.         languages: ['cpp'],
  30.         ignoreUnescapedHTML: true, // anchors
  31.       });
  32.       for(const codeBlock of codeBlocks) {
  33.         const anchors = codeBlock.querySelectorAll('a');
  34.         hljs.highlightElement(codeBlock);
  35.         
  36.         if (anchors.length === 0) continue;
  37.         const urlMap = new Map(Array.from(anchors, anchor => [anchor.textContent, anchor.href]));
  38.         console.info(urlMap);
  39.  
  40.         for (const strEl of codeBlock.querySelectorAll('.hljs-string')) {
  41.           const fileName = strEl.textContent.slice(1, -1);
  42.           console.info('searching for %s...', fileName);
  43.           if (urlMap.has(fileName)) {
  44.             const newAnchor = document.createElement('a');
  45.             newAnchor.href = urlMap.get(fileName);
  46.             newAnchor.style.borderBottom = '1px dotted';
  47.             strEl.insertAdjacentElement('afterend', newAnchor);
  48.             newAnchor.appendChild(strEl);
  49.           }
  50.         }
  51.       }
  52.     },
  53.   });
  54.   document.head.appendChild(hljsScript);
  55. }
  56.  
  57. if (document.readyState === 'loading' && !document.head) {
  58.   addEventListener('DOMContentLoaded', main);  
  59. } else {
  60.   main();
  61. }