| 137 | } |
| 138 | |
| 139 | function change(mirror, changes) { |
| 140 | var to = changes.to; |
| 141 | var from = changes.from; |
| 142 | var text = changes.text; |
| 143 | var next = changes.next; |
| 144 | var length = text.length; |
| 145 | |
| 146 | if (user) { |
| 147 | if (from.line < line || from.ch < ch) mirror.undo(); |
| 148 | else if (length-- > 1) { |
| 149 | mirror.undo(); |
| 150 | |
| 151 | var ln = mirror.getLine(line).slice(ch); |
| 152 | text[0] = ln.slice(0, from.ch) + text[0]; |
| 153 | |
| 154 | for (var i = 0; i < length; i++) { |
| 155 | mirror.setLine(line, text[i]); |
| 156 | enter(); |
| 157 | } |
| 158 | |
| 159 | mirror.setLine(line, text[length] + ln.slice(to.ch)); |
| 160 | } |
| 161 | } |
| 162 | |
| 163 | if (next) change(mirror, next); |
| 164 | } |
| 165 | |
| 166 | function print(message, className) { |
| 167 | var mode = user; |