Function charWidth

external/.scrollLibs.js:4310–4323

(display)

  // Compute the default character width.
  function charWidth(display) {
    if (display.cachedCharWidth != null) {
      return display.cachedCharWidth
    }
    var anchor = elt("span", "xxxxxxxxxx")
    var pre = elt("pre", [anchor])
    removeChildrenAndAdd(display.measure, pre)
    var rect = anchor.getBoundingClientRect(),
      width = (rect.right - rect.left) / 10
    if (width > 2) {
      display.cachedCharWidth = width
    }
    return width || 10
  }

  // Do a bulk-read of the DOM positions and sizes needed to draw the
  // view, so that we don't interleave reading and writing to the DOM.