Function setDocumentHeight

tools/pythonauto/static/codemirrorepl/codemirror.js:652–655

(cm, measure)

  }

  function setDocumentHeight(cm, measure) {
    cm.display.sizer.style.minHeight = cm.display.heightForcer.style.top = measure.docHeight + "px";
    cm.display.gutters.style.height = Math.max(measure.docHeight, measure.clientHeight - scrollerCutOff) + "px";
  }

  // Read the actual heights of the rendered lines, and update their
  // stored heights to match.