Function updateLineHeight

tools/pythonauto/static/codemirror/codemirror.js:5237–5240

(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;