()
| 2080 | } |
| 2081 | |
| 2082 | private undo(): void { |
| 2083 | this.exitHistoryBrowsing(); |
| 2084 | const snapshot = this.undoStack.pop(); |
| 2085 | if (!snapshot) return; |
| 2086 | Object.assign(this.state, snapshot); |
| 2087 | this.lastAction = null; |
| 2088 | this.preferredVisualCol = null; |
| 2089 | if (this.onChange) { |
| 2090 | this.onChange(this.getText()); |
| 2091 | } |
| 2092 | } |
| 2093 | |
| 2094 | /** |
| 2095 | * Jump to the first occurrence of a character in the specified direction. |
no test coverage detected