(cm)
| 3537 | |
| 3538 | // Called when the window resizes |
| 3539 | function onResize(cm) { |
| 3540 | var d = cm.display; |
| 3541 | if (d.lastWrapHeight == d.wrapper.clientHeight && d.lastWrapWidth == d.wrapper.clientWidth) |
| 3542 | return; |
| 3543 | // Might be a text scaling operation, clear size caches. |
| 3544 | d.cachedCharWidth = d.cachedTextHeight = d.cachedPaddingH = null; |
| 3545 | d.scrollbarsClipped = false; |
| 3546 | cm.setSize(); |
| 3547 | } |
| 3548 | |
| 3549 | // MOUSE EVENTS |
| 3550 |