Function updateLineHeight

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:535–539

(line, height)

        function getLine(n) { return getLineAt(doc, n); }
        function updateLineHeight(line, height) {
            gutterDirty = true;
            var diff = height - line.height;
            for (var n = line; n; n = n.parent) n.height += diff;
        }

        function setValue(code) {
            var top = {line: 0, ch: 0};