(op)
| 3878 | } |
| 3879 | |
| 3880 | function endOperation_finish(op) { |
| 3881 | var cm = op.cm, display = cm.display, doc = cm.doc; |
| 3882 | |
| 3883 | if (op.updatedDisplay) { postUpdateDisplay(cm, op.update); } |
| 3884 | |
| 3885 | // Abort mouse wheel delta measurement, when scrolling explicitly |
| 3886 | if (display.wheelStartX != null && (op.scrollTop != null || op.scrollLeft != null || op.scrollToPos)) |
| 3887 | { display.wheelStartX = display.wheelStartY = null; } |
| 3888 | |
| 3889 | // Propagate the scroll position to the actual DOM scroller |
| 3890 | if (op.scrollTop != null) { setScrollTop(cm, op.scrollTop, op.forceScroll); } |
| 3891 | |
| 3892 | if (op.scrollLeft != null) { setScrollLeft(cm, op.scrollLeft, true, true); } |
| 3893 | // If we need to scroll a specific position into view, do so. |
| 3894 | if (op.scrollToPos) { |
| 3895 | var rect = scrollPosIntoView(cm, clipPos(doc, op.scrollToPos.from), |
| 3896 | clipPos(doc, op.scrollToPos.to), op.scrollToPos.margin); |
| 3897 | maybeScrollWindow(cm, rect); |
| 3898 | } |
| 3899 | |
| 3900 | // Fire events for markers that are hidden/unidden by editing or |
| 3901 | // undoing |
| 3902 | var hidden = op.maybeHiddenMarkers, unhidden = op.maybeUnhiddenMarkers; |
| 3903 | if (hidden) { for (var i = 0; i < hidden.length; ++i) |
| 3904 | { if (!hidden[i].lines.length) { signal(hidden[i], "hide"); } } } |
| 3905 | if (unhidden) { for (var i$1 = 0; i$1 < unhidden.length; ++i$1) |
| 3906 | { if (unhidden[i$1].lines.length) { signal(unhidden[i$1], "unhide"); } } } |
| 3907 | |
| 3908 | if (display.wrapper.offsetHeight) |
| 3909 | { doc.scrollTop = cm.display.scroller.scrollTop; } |
| 3910 | |
| 3911 | // Fire change events, and delayed event handlers |
| 3912 | if (op.changeObjs) |
| 3913 | { signal(cm, "changes", cm, op.changeObjs); } |
| 3914 | if (op.update) |
| 3915 | { op.update.finish(); } |
| 3916 | } |
| 3917 | |
| 3918 | // Run the given function in an operation |
| 3919 | function runInOp(cm, f) { |
no test coverage detected