| 538 | // Re-synchronize the fake scrollbars with the actual size of the |
| 539 | // content. |
| 540 | function updateScrollbarsInner(cm, measure) { |
| 541 | var d = cm.display; |
| 542 | var sizes = d.scrollbars.update(measure); |
| 543 | |
| 544 | d.sizer.style.paddingRight = (d.barWidth = sizes.right) + "px"; |
| 545 | d.sizer.style.paddingBottom = (d.barHeight = sizes.bottom) + "px"; |
| 546 | |
| 547 | if (sizes.right && sizes.bottom) { |
| 548 | d.scrollbarFiller.style.display = "block"; |
| 549 | d.scrollbarFiller.style.height = sizes.bottom + "px"; |
| 550 | d.scrollbarFiller.style.width = sizes.right + "px"; |
| 551 | } else d.scrollbarFiller.style.display = ""; |
| 552 | if (sizes.bottom && cm.options.coverGutterNextToScrollbar && cm.options.fixedGutter) { |
| 553 | d.gutterFiller.style.display = "block"; |
| 554 | d.gutterFiller.style.height = sizes.bottom + "px"; |
| 555 | d.gutterFiller.style.width = measure.gutterWidth + "px"; |
| 556 | } else d.gutterFiller.style.display = ""; |
| 557 | } |
| 558 | |
| 559 | // Compute the lines that are visible in a given viewport (defaults |
| 560 | // the the current scroll position). viewport may contain top, |