| OLD | NEW |
| 1 /* Functionality for finding, storing, and restoring selections | 1 /* Functionality for finding, storing, and restoring selections |
| 2 * | 2 * |
| 3 * This does not provide a generic API, just the minimal functionality | 3 * This does not provide a generic API, just the minimal functionality |
| 4 * required by the CodeMirror system. | 4 * required by the CodeMirror system. |
| 5 */ | 5 */ |
| 6 | 6 |
| 7 // Namespace object. | 7 // Namespace object. |
| 8 var select = {}; | 8 var select = {}; |
| 9 | 9 |
| 10 (function() { | 10 (function() { |
| (...skipping 463 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
| 474 } | 474 } |
| 475 | 475 |
| 476 to = to || from; | 476 to = to || from; |
| 477 if (setPoint(to.node, to.offset, "End") && setPoint(from.node, from.offset
, "Start")) | 477 if (setPoint(to.node, to.offset, "End") && setPoint(from.node, from.offset
, "Start")) |
| 478 selectRange(range, win); | 478 selectRange(range, win); |
| 479 }; | 479 }; |
| 480 | 480 |
| 481 select.scrollToCursor = function(container) { | 481 select.scrollToCursor = function(container) { |
| 482 var body = container.ownerDocument.body, win = container.ownerDocument.def
aultView; | 482 var body = container.ownerDocument.body, win = container.ownerDocument.def
aultView; |
| 483 var element = select.selectionTopNode(container, true) || container.firstC
hild; | 483 var element = select.selectionTopNode(container, true) || container.firstC
hild; |
| 484 | 484 |
| 485 // In Opera, BR elements *always* have a scrollTop property of zero. Go Op
era. | 485 // In Opera, BR elements *always* have a scrollTop property of zero. Go Op
era. |
| 486 while (element && !element.offsetTop) | 486 while (element && !element.offsetTop) |
| 487 element = element.previousSibling; | 487 element = element.previousSibling; |
| 488 | 488 |
| 489 var y = 0, pos = element; | 489 var y = 0, pos = element; |
| 490 while (pos && pos.offsetParent) { | 490 while (pos && pos.offsetParent) { |
| 491 y += pos.offsetTop; | 491 y += pos.offsetTop; |
| 492 pos = pos.offsetParent; | 492 pos = pos.offsetParent; |
| 493 } | 493 } |
| 494 | 494 |
| 495 var screen_y = y - body.scrollTop; | 495 var screen_y = y - body.scrollTop; |
| 496 if (screen_y < 0 || screen_y > win.innerHeight - 10) | 496 if (screen_y < 0 || screen_y > win.innerHeight - 10) |
| 497 win.scrollTo(0, y); | 497 win.scrollTo(0, y); |
| 498 }; | 498 }; |
| 499 } | 499 } |
| 500 }()); | 500 }()); |
| OLD | NEW |