| 849 | updateLinesNoUndo(from, to, newText, selFrom, selTo); |
| 850 | } |
| 851 | function unredoHelper(from, to) { |
| 852 | if (!from.length) return; |
| 853 | var set = from.pop(), out = []; |
| 854 | for (var i = set.length - 1; i >= 0; i -= 1) { |
| 855 | var change = set[i]; |
| 856 | var replaced = [], end = change.start + change.added; |
| 857 | doc.iter(change.start, end, function(line) { replaced.push(line.text); }); |
| 858 | out.push({start: change.start, added: change.old.length, old: replaced}); |
| 859 | var pos = clipPos({line: change.start + change.old.length - 1, |
| 860 | ch: editEnd(replaced[replaced.length-1], change.old[change.old.length-1])}); |
| 861 | updateLinesNoUndo({line: change.start, ch: 0}, {line: end - 1, ch: getLine(end-1).text.length}, change.old, pos, pos); |
| 862 | } |
| 863 | updateInput = true; |
| 864 | to.push(out); |
| 865 | } |
| 866 | function undo() {unredoHelper(history.done, history.undone);} |
| 867 | function redo() {unredoHelper(history.undone, history.done);} |
| 868 | |