Function updateLineHeight

static/js/codemirror/codemirror.js:4588–4591

(line, height)

  }

  function updateLineHeight(line, height) {
    var diff = height - line.height;
    for (var n = line; n; n = n.parent) n.height += diff;
  }

  function lineNo(line) {
    if (line.parent == null) return null;