398 |
buffer = newBuf; |
buffer = newBuf; |
399 |
|
|
400 |
// Update the marks after the gapEnd. |
// Update the marks after the gapEnd. |
401 |
int index = Collections.binarySearch(positions, new Integer(gapEnd)); |
int index = Collections.binarySearch(positions, |
402 |
|
new GapContentPosition(gapEnd)); |
403 |
if (index < 0) |
if (index < 0) |
404 |
{ |
{ |
405 |
index = -(index + 1); |
index = -(index + 1); |
423 |
|
|
424 |
// Update the positions between newGapEnd and (old) gapEnd. The marks |
// Update the positions between newGapEnd and (old) gapEnd. The marks |
425 |
// must be shifted by (gapEnd - newGapEnd). |
// must be shifted by (gapEnd - newGapEnd). |
426 |
int index1 = Collections.binarySearch(positions, new Integer(gapEnd)); |
int index1 = Collections.binarySearch(positions, |
427 |
int index2 = Collections.binarySearch(positions, new Integer(newGapEnd)); |
new GapContentPosition(gapEnd)); |
428 |
|
int index2 = Collections.binarySearch(positions, |
429 |
|
new GapContentPosition(newGapEnd)); |
430 |
int i1 = Math.min(index1, index2); |
int i1 = Math.min(index1, index2); |
431 |
int i2 = Math.max(index1, index2); |
int i2 = Math.max(index1, index2); |
432 |
for (ListIterator i = positions.listIterator(i1); i.hasNext();) |
for (ListIterator i = positions.listIterator(i1); i.hasNext();) |