Function changeLine

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:1682–1690

(handle, op)

        }

        function changeLine(handle, op) {
            var no = handle, line = handle;
            if (typeof handle == "number") line = getLine(clipLine(handle));
            else no = lineNo(handle);
            if (no == null) return null;
            if (op(line, no)) changes.push({from: no, to: no + 1});
            else return null;
            return line;
        }
        function setLineClass(handle, className, bgClassName) {
            return changeLine(handle, function(line) {
                if (line.className != className || line.bgClassName != bgClassName) {