(line, text, markedSpans, estimateHeight)
| 6721 | // invalidates cached information and tries to re-estimate the |
| 6722 | // line's height. |
| 6723 | function updateLine(line, text, markedSpans, estimateHeight) { |
| 6724 | line.text = text; |
| 6725 | if (line.stateAfter) line.stateAfter = null; |
| 6726 | if (line.styles) line.styles = null; |
| 6727 | if (line.order != null) line.order = null; |
| 6728 | detachMarkedSpans(line); |
| 6729 | attachMarkedSpans(line, markedSpans); |
| 6730 | var estHeight = estimateHeight ? estimateHeight(line) : 1; |
| 6731 | if (estHeight != line.height) updateLineHeight(line, estHeight); |
| 6732 | } |
| 6733 | |
| 6734 | // Detach a line from the document tree and its markers. |
| 6735 | function cleanUpLine(line) { |
no test coverage detected