642 |
|
|
643 |
int index1 = Collections.binarySearch(positions, |
int index1 = Collections.binarySearch(positions, |
644 |
new GapContentPosition(offset)); |
new GapContentPosition(offset)); |
|
int index2 = Collections.binarySearch(positions, |
|
|
new GapContentPosition(endOffset)); |
|
645 |
if (index1 < 0) |
if (index1 < 0) |
646 |
index1 = -(index1 + 1); |
index1 = -(index1 + 1); |
|
if (index2 < 0) |
|
|
index2 = -(index2 + 1); |
|
647 |
for (ListIterator i = positions.listIterator(index1); i.hasNext();) |
for (ListIterator i = positions.listIterator(index1); i.hasNext();) |
648 |
{ |
{ |
|
if (i.nextIndex() > index2) |
|
|
break; |
|
|
|
|
649 |
GapContentPosition p = (GapContentPosition) i.next(); |
GapContentPosition p = (GapContentPosition) i.next(); |
650 |
|
if (p.mark > endOffset) |
651 |
|
break; |
652 |
if (p.mark >= offset && p.mark <= endOffset) |
if (p.mark >= offset && p.mark <= endOffset) |
653 |
res.add(p); |
res.add(p); |
654 |
} |
} |