| 5971 | eventMixin(SharedTextMarker); |
| 5972 | |
| 5973 | function markTextShared(doc, from, to, options, type) { |
| 5974 | options = copyObj(options); |
| 5975 | options.shared = false; |
| 5976 | var markers = [markText(doc, from, to, options, type)], primary = markers[0]; |
| 5977 | var widget = options.widgetNode; |
| 5978 | linkedDocs(doc, function (doc) { |
| 5979 | if (widget) { options.widgetNode = widget.cloneNode(true); } |
| 5980 | markers.push(markText(doc, clipPos(doc, from), clipPos(doc, to), options, type)); |
| 5981 | for (var i = 0; i < doc.linked.length; ++i) |
| 5982 | { if (doc.linked[i].isParent) { return } } |
| 5983 | primary = lst(markers); |
| 5984 | }); |
| 5985 | return new SharedTextMarker(markers, primary) |
| 5986 | } |
| 5987 | |
| 5988 | function findSharedMarkers(doc) { |
| 5989 | return doc.findMarks(Pos(doc.first, 0), doc.clipPos(Pos(doc.lastLine())), function (m) { return m.parent; }) |