Function paddingTop

static/js/codemirror/codemirror.js:933–933

(display)

  // POSITION MEASUREMENT
  
  function paddingTop(display) {return display.lineSpace.offsetTop;}
  function paddingLeft(display) {
    var e = removeChildrenAndAdd(display.measure, elt("pre", null, null, "text-align: left")).appendChild(elt("span", "x"));
    return e.offsetLeft;