diff --git a/lib/codemirror.js b/lib/codemirror.js index 164da2e13a7893d0eae374962298ff517f19f0a0..590400a2f9dc5989014810703a1946258dad74c0 100644 --- a/lib/codemirror.js +++ b/lib/codemirror.js @@ -193,6 +193,7 @@ d.reportedViewFrom = d.reportedViewTo = doc.first; // Information about the rendered lines. d.view = []; + d.renderedView = null; // Holds info about a single rendered line when it was rendered // for measurement, while not in view. d.externalMeasured = null; @@ -671,7 +672,7 @@ if (!update.force && update.visible.from >= display.viewFrom && update.visible.to <= display.viewTo && (display.updateLineNumbers == null || display.updateLineNumbers >= display.viewTo) && - countDirtyView(cm) == 0) + display.renderedView == display.view && countDirtyView(cm) == 0) return false; if (maybeUpdateLineNumberWidth(cm)) { @@ -699,7 +700,7 @@ cm.display.mover.style.top = display.viewOffset + "px"; var toUpdate = countDirtyView(cm); - if (!different && toUpdate == 0 && !update.force && + if (!different && toUpdate == 0 && !update.force && display.renderedView == display.view && (display.updateLineNumbers == null || display.updateLineNumbers >= display.viewTo)) return false; @@ -709,6 +710,7 @@ if (toUpdate > 4) display.lineDiv.style.display = "none"; patchDisplay(cm, display.updateLineNumbers, update.dims); if (toUpdate > 4) display.lineDiv.style.display = ""; + display.renderedView = display.view; // There might have been a widget with a focused element that got // hidden or updated, if so re-focus it. if (focused && activeElt() != focused && focused.offsetHeight) focused.focus();