Function updateGutterSpace

external/.scrollLibs.js:6094–6097

(cm)

  }

  function updateGutterSpace(cm) {
    var width = cm.display.gutters.offsetWidth
    cm.display.sizer.style.marginLeft = width + "px"
  }

  function setDocumentHeight(cm, measure) {
    cm.display.sizer.style.minHeight = measure.docHeight + "px"