function pushEdit(startOffset: Length, endOffset: Length, newLength: Length): void {
if (result.length > 0 && lengthEquals(result[result.length - 1].endOffset, startOffset)) {
result[result.length - 1] = new TextEditInfo(lastResult.startOffset, endOffset, lengthAdd(lastResult.newLength, newLength));
} else {
result.push({ startOffset, endOffset, newLength });