Function updateGutter

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:1287–1323

()

        }

        function updateGutter() {
            if (!options.gutter && !options.lineNumbers) return;
            var hText = mover.offsetHeight, hEditor = scroller.clientHeight;
            gutter.style.height = (hText - hEditor < 2 ? hEditor : hText) + "px";
            var html = [], i = showingFrom, normalNode;
            doc.iter(showingFrom, Math.max(showingTo, showingFrom + 1), function(line) {
                if (line.hidden) {
                    html.push("<pre></pre>");
                } else {
                    var marker = line.gutterMarker;
                    var text = options.lineNumbers ? i + options.firstLineNumber : null;
                    if (marker && marker.text)
                        text = marker.text.replace("%N%", text != null ? text : "");
                    else if (text == null)
                        text = "\u00a0";
                    html.push((marker && marker.style ? '<pre class="' + marker.style + '">' : "<pre>"), text);
                    for (var j = 1; j < line.height; ++j) html.push("<br/>&#160;");
                    html.push("</pre>");
                    if (!marker) normalNode = i;
                }
                ++i;
            });
            gutter.style.display = "none";
            gutterText.innerHTML = html.join("");
            // Make sure scrolling doesn't cause number gutter size to pop
            if (normalNode != null) {
                var node = gutterText.childNodes[normalNode - showingFrom];
                var minwidth = String(doc.size).length, val = eltText(node), pad = "";
                while (val.length + pad.length < minwidth) pad += "\u00a0";
                if (pad) node.insertBefore(document.createTextNode(pad), node.firstChild);
            }
            gutter.style.display = "";
            var resized = Math.abs((parseInt(lineSpace.style.marginLeft) || 0) - gutter.offsetWidth) > 2;
            lineSpace.style.marginLeft = gutter.offsetWidth + "px";
            gutterDirty = false;
            return resized;
        }
        function updateSelection() {
            var collapsed = posEq(sel.from, sel.to);
            var fromPos = localCoords(sel.from, true);