47 |
public static final String lineLimitAttribute = "lineLimit"; |
public static final String lineLimitAttribute = "lineLimit"; |
48 |
public static final String tabSizeAttribute = "tabSize"; |
public static final String tabSizeAttribute = "tabSize"; |
49 |
|
|
50 |
private Element rootElement; |
private BranchElement rootElement; |
51 |
private int tabSize; |
private int tabSize; |
52 |
|
|
53 |
public PlainDocument() |
public PlainDocument() |
59 |
{ |
{ |
60 |
super(content); |
super(content); |
61 |
tabSize = 8; |
tabSize = 8; |
62 |
rootElement = createDefaultRoot(); |
rootElement = (BranchElement) createDefaultRoot(); |
63 |
} |
} |
64 |
|
|
65 |
private void reindex() |
private void reindex() |
114 |
|
|
115 |
protected void removeUpdate(DefaultDocumentEvent event) |
protected void removeUpdate(DefaultDocumentEvent event) |
116 |
{ |
{ |
|
reindex(); |
|
|
|
|
117 |
super.removeUpdate(event); |
super.removeUpdate(event); |
118 |
|
|
119 |
|
int p0 = event.getOffset(); |
120 |
|
int p1 = event.getLength() + p0; |
121 |
|
int len = event.getLength(); |
122 |
|
|
123 |
|
// check if we must collapse some elements |
124 |
|
int i1 = rootElement.getElementIndex(p0); |
125 |
|
int i2 = rootElement.getElementIndex(p1); |
126 |
|
if (i1 != i2) |
127 |
|
{ |
128 |
|
Element el1 = rootElement.getElement(i1); |
129 |
|
Element el2 = rootElement.getElement(i2); |
130 |
|
int start = el1.getStartOffset(); |
131 |
|
int end = el2.getEndOffset(); |
132 |
|
// collapse elements if the removal spans more than 1 line |
133 |
|
Element newEl = createLeafElement(rootElement, |
134 |
|
SimpleAttributeSet.EMPTY, |
135 |
|
start, end - len); |
136 |
|
rootElement.replace(start, end - start, new Element[]{ newEl }); |
137 |
|
} |
138 |
|
else |
139 |
|
{ |
140 |
|
// otherwise only adjust indices of the element |
141 |
|
LeafElement el1 = (LeafElement) rootElement.getElement(i1); |
142 |
|
el1.end -= len; |
143 |
|
} |
144 |
|
|
145 |
|
// reindex remaining elements |
146 |
|
for (int i = rootElement.getElementIndex(p0) + 1; |
147 |
|
i < rootElement.getElementCount(); i++) |
148 |
|
{ |
149 |
|
LeafElement el = (LeafElement) rootElement.getElement(i); |
150 |
|
el.start -= len; |
151 |
|
el.end -= len; |
152 |
|
} |
153 |
|
|
154 |
} |
} |
155 |
|
|
156 |
public Element getDefaultRootElement() |
public Element getDefaultRootElement() |