Function updateLine

static/js/codemirror/codemirror.js:3837–3847

(line, text, markedSpans, estimateHeight)

  }

  function updateLine(line, text, markedSpans, estimateHeight) {
    line.text = text;
    if (line.stateAfter) line.stateAfter = null;
    if (line.styles) line.styles = null;
    if (line.order != null) line.order = null;
    detachMarkedSpans(line);
    attachMarkedSpans(line, markedSpans);
    var estHeight = estimateHeight ? estimateHeight(line) : 1;
    if (estHeight != line.height) updateLineHeight(line, estHeight);
    signalLater(line, "change");
  }

  function cleanUpLine(line) {
    line.parent = null;