Function setDocumentHeight

external/.scrollLibs.js:6099–6103

(cm, measure)

  }

  function setDocumentHeight(cm, measure) {
    cm.display.sizer.style.minHeight = measure.docHeight + "px"
    cm.display.heightForcer.style.top = measure.docHeight + "px"
    cm.display.gutters.style.height = measure.docHeight + cm.display.barHeight + scrollGap(cm) + "px"
  }

  // Rebuild the gutter elements, ensure the margin to the left of the
  // code matches their width.