endHistoryBatch method
void
endHistoryBatch()
Finishes a history batch.
Implementation
void endHistoryBatch() {
if (_historyBatchDepth == 0) return;
_historyBatchDepth -= 1;
if (_historyBatchDepth > 0) return;
final snapshot = _historyBatchSnapshot;
_historyBatchSnapshot = null;
if (snapshot == null) return;
_pushUndo(snapshot);
_redoStack.clear();
}