Function stringWidth

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:1744–1748

(str)

        }

        function stringWidth(str) {
            measure.innerHTML = "<pre><span>x</span></pre>";
            measure.firstChild.firstChild.firstChild.nodeValue = str;
            return measure.firstChild.firstChild.offsetWidth || 10;
        }
        // These are used to go from pixel positions to character
        // positions, taking varying character widths into account.
        function charFromX(line, x) {