135 |
start, end - len); |
start, end - len); |
136 |
rootElement.replace(i1, i2 - i1, new Element[]{ newEl }); |
rootElement.replace(i1, i2 - i1, new Element[]{ newEl }); |
137 |
} |
} |
|
else |
|
|
{ |
|
|
// otherwise only adjust indices of the element |
|
|
LeafElement el1 = (LeafElement) rootElement.getElement(i1); |
|
|
el1.end -= len; |
|
|
} |
|
|
|
|
|
// reindex remaining elements |
|
|
for (int i = rootElement.getElementIndex(p0) + 1; |
|
|
i < rootElement.getElementCount(); i++) |
|
|
{ |
|
|
LeafElement el = (LeafElement) rootElement.getElement(i); |
|
|
el.start -= len; |
|
|
el.end -= len; |
|
|
} |
|
|
|
|
138 |
} |
} |
139 |
|
|
140 |
public Element getDefaultRootElement() |
public Element getDefaultRootElement() |