(display)
| 2522 | function paddingTop(display) {return display.lineSpace.offsetTop;} |
| 2523 | function paddingVert(display) {return display.mover.offsetHeight - display.lineSpace.offsetHeight;} |
| 2524 | function paddingH(display) { |
| 2525 | if (display.cachedPaddingH) return display.cachedPaddingH; |
| 2526 | var e = removeChildrenAndAdd(display.measure, elt("pre", "x")); |
| 2527 | var style = window.getComputedStyle ? window.getComputedStyle(e) : e.currentStyle; |
| 2528 | var data = {left: parseInt(style.paddingLeft), right: parseInt(style.paddingRight)}; |
| 2529 | if (!isNaN(data.left) && !isNaN(data.right)) display.cachedPaddingH = data; |
| 2530 | return data; |
| 2531 | } |
| 2532 | |
| 2533 | function scrollGap(cm) { return scrollerGap - cm.display.nativeBarWidth; } |
| 2534 | function displayWidth(cm) { |
no test coverage detected