Function highlightLines

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:2001–2007

(start, end)

            return state;
        }
        function highlightLines(start, end) {
            var state = getStateBefore(start);
            doc.iter(start, end, function(line) {
                line.highlight(mode, state, options.tabSize);
                line.stateAfter = copyState(mode, state);
            });
        }
        function highlightWorker() {
            var end = +new Date + options.workTime;
            var foundWork = work.length;