| 8131 | eventMixin(SharedTextMarker) |
| 8132 | |
| 8133 | function markTextShared(doc, from, to, options, type) { |
| 8134 | options = copyObj(options) |
| 8135 | options.shared = false |
| 8136 | var markers = [markText(doc, from, to, options, type)], |
| 8137 | primary = markers[0] |
| 8138 | var widget = options.widgetNode |
| 8139 | linkedDocs(doc, function (doc) { |
| 8140 | if (widget) { |
| 8141 | options.widgetNode = widget.cloneNode(true) |
| 8142 | } |
| 8143 | markers.push(markText(doc, clipPos(doc, from), clipPos(doc, to), options, type)) |
| 8144 | for (var i = 0; i < doc.linked.length; ++i) { |
| 8145 | if (doc.linked[i].isParent) { |
| 8146 | return |
| 8147 | } |
| 8148 | } |
| 8149 | primary = lst(markers) |
| 8150 | }) |
| 8151 | return new SharedTextMarker(markers, primary) |
| 8152 | } |
| 8153 | |
| 8154 | function findSharedMarkers(doc) { |
| 8155 | return doc.findMarks(Pos(doc.first, 0), doc.clipPos(Pos(doc.lastLine())), function (m) { |