| 624 | } |
| 625 | |
| 626 | function collapseSingle(cm, from, to) { |
| 627 | cm.addLineClass(from, "wrap", "CodeMirror-merge-collapsed-line"); |
| 628 | var widget = document.createElement("span"); |
| 629 | widget.className = "CodeMirror-merge-collapsed-widget"; |
| 630 | widget.title = "Identical text collapsed. Click to expand."; |
| 631 | var mark = cm.markText(Pos(from, 0), Pos(to - 1), { |
| 632 | inclusiveLeft: true, |
| 633 | inclusiveRight: true, |
| 634 | replacedWith: widget, |
| 635 | clearOnEnter: true |
| 636 | }); |
| 637 | function clear() { |
| 638 | mark.clear(); |
| 639 | cm.removeLineClass(from, "wrap", "CodeMirror-merge-collapsed-line"); |
| 640 | } |
| 641 | widget.addEventListener("click", clear); |
| 642 | return {mark: mark, clear: clear}; |
| 643 | } |
| 644 | |
| 645 | function collapseStretch(size, editors) { |
| 646 | var marks = []; |