Improves TeX preview on nLab

nLabTexImprover.user.js

// ==UserScript==
// @name         nLab TeX Preview Improver
// @version      2025-12-22
// @description  Improves the TeX source previewer on the nLab website.
// @author       jrr6
// @match        https://ncatlab.org/*
// @grant        none
// @downloadURL  https://gist.github.com/jrr6/c0273e1d6c04c86b84aea692bd11b9c6/raw/nLabTexImprover.user.js
// @updateURL    https://gist.github.com/jrr6/c0273e1d6c04c86b84aea692bd11b9c6/raw/nLabTexImprover.user.js
// ==/UserScript==



(function() {
    'use strict';

    function replaceTexSourcePreview() {
        $$('math').each( function(math){Event.stopObserving(math, 'dblclick') } )
        $$('math').each( function(math){Event.observe(math, 'dblclick', grabTex) } )
        function grabTex(event){
            let math = this
            Event.stopObserving(math, 'dblclick', grabTex)
            var tex = this.firstElementChild.lastElementChild.textContent;
            const div = document.createElement('div')
            div.style.position = 'fixed'
            div.style.top = '50%'
            div.style.left = '50%'
            div.style.transform = 'translate(-50%, -200%)'
            div.style.background = 'white'
            div.style.padding = '0 2em 1em 2em'
            div.style.border = '1px solid black'
            div.style.width = '50%'
            div.innerHTML = `
			<h1 style="display:inline-block;">TeX Source</h1>
			<button style="margin-top: 2.5em; display: inline-block; margin-left: 1em;" onclick="navigator.clipboard.writeText(document.getElementById('injected-tex-source').textContent)">Copy</button>
      <code style="clear: both; display: block; font-size: 12px;" id="injected-tex-source"></code>
		`
            div.getElementsByTagName('code')[0].textContent = tex
            document.body.appendChild(div)
            document.getElementById('Container').style.filter = 'blur(1px)'
            function hidePopup(evt) {
                if (!div.contains(evt.target)) {
                    document.body.removeChild(div)
                    document.getElementById('Container').style.filter = ''
                    document.removeEventListener('click', hidePopup, false)
                    Event.observe(math, 'dblclick', grabTex)
                }
            }
            document.addEventListener('click', hidePopup, false)
        }
    }

    replaceTexSourcePreview();
})();