|
1
21
22 package org.armedbear.j;
23
24 import java.util.List  ;
25
26 public final class Region implements Constants
27 {
28 private final Buffer buffer;
29 private final Position begin;
30 private final Line beginLine;
31 private final int beginOffset;
32 private Position end;
33 private Line endLine;
34 private int endOffset;
35 private boolean isColumnRegion;
36 private int beginCol = -1;
37 private int endCol = -1;
38
39 public Region(Buffer buffer, Position pos1, Position pos2)
42 {
43 this.buffer = buffer;
44 if (buffer.needsRenumbering())
45 buffer.renumber();
46 if (pos1.isBefore(pos2)) {
47 begin = new Position(pos1);
48 end = new Position(pos2);
49 } else {
50 begin = new Position(pos2);
51 end = new Position(pos1);
52 }
53 beginLine = begin.getLine();
54 beginOffset = begin.getOffset();
55 endLine = end.getLine();
56 endOffset = end.getOffset();
57 }
58
59 public Region(Editor editor)
60 {
61 this(editor.getBuffer(), editor.getMark(), editor.getDot());
62 if (editor.isColumnSelection()) {
63 isColumnRegion = true;
64 if (begin.equals(editor.getMark())) {
65 beginCol = buffer.getCol(begin);
66 endCol = editor.getDisplay().getAbsoluteCaretCol();
67 } else {
68 beginCol = editor.getDisplay().getAbsoluteCaretCol();
69 endCol = buffer.getCol(end);
70 }
71 }
72 }
73
74 public final Buffer getBuffer()
75 {
76 return buffer;
77 }
78
79 public final Position getBegin()
80 {
81 return begin;
82 }
83
84 public final Line getBeginLine()
85 {
86 return beginLine;
87 }
88
89 public final int getBeginLineNumber()
90 {
91 return beginLine.lineNumber();
92 }
93
94 public final int getBeginOffset()
95 {
96 return beginOffset;
97 }
98
99 public final int getBeginCol()
100 {
101 if (beginCol < 0)
102 beginCol = buffer.getCol(begin);
103 return beginCol;
104 }
105
106 public final Position getEnd()
107 {
108 return end;
109 }
110
111 public final void setEnd(Position pos)
112 {
113 end = pos;
114 endLine = end.getLine();
115 endOffset = end.getOffset();
116 endCol = -1;
117 }
118
119 public final Line getEndLine()
120 {
121 return endLine;
122 }
123
124 public final int getEndLineNumber()
125 {
126 return endLine.lineNumber();
127 }
128
129 public final int getEndOffset()
130 {
131 return endOffset;
132 }
133
134 public final void setEndOffset(int offset)
135 {
136 end.setOffset(offset);
137 endOffset = offset;
138 }
139
140 public final int getEndCol()
141 {
142 if (endCol < 0)
143 endCol = buffer.getCol(end);
144 return endCol;
145 }
146
147 public final boolean isColumnRegion()
148 {
149 return isColumnRegion;
150 }
151
152 public final boolean isLineRegion()
153 {
154 return beginOffset == 0 && endOffset == 0;
155 }
156
157 public String toString()
158 {
159 if (beginLine == endLine)
160 return beginLine.substring(beginOffset, endOffset);
161
162 FastStringBuffer sb = new FastStringBuffer();
163 if (isColumnRegion) {
164 for (Line line = beginLine; line != null; line = line.next()) {
165 sb.append(getTextInRegion(line));
166 sb.append('\n');
167 if (line == getEndLine())
168 break;
169 }
170 } else {
171 sb.append(beginLine.substring(beginOffset));
172 sb.append('\n');
173 Line line = beginLine.next();
174 while (line != endLine && line != null) {
175 sb.append(line.getText());
176 sb.append('\n');
177 line = line.next();
178 }
179 if (line == endLine)
180 sb.append(line.substring(0, endOffset));
181 }
182 return sb.toString();
183 }
184
185 private String getTextInRegion(Line line)
186 {
187 String text = Utilities.detab(line.getText(), buffer.getTabWidth());
188 if (text.length() > getEndCol())
189 return text.substring(getBeginCol(), getEndCol());
190 else if (text.length() > getBeginCol())
191 return text.substring(getBeginCol());
192 else
193 return "";
194 }
195
196 public boolean adjustMarker(Position pos)
197 {
198 if (pos == null)
199 return false;
200 final Line line = pos.getLine();
201 final int offset = pos.getOffset();
202 if (line == null)
203 return false;
204 if (line == beginLine) {
205 if (line == endLine && offset > endOffset) {
206 pos.setOffset(offset - (endOffset - beginOffset));
207 return true;
208 }
209 if (offset > beginOffset) {
210 pos.setOffset(beginOffset);
211 return true;
212 }
213 return false;
214 }
215 if (line == endLine) {
216 if (offset <= endOffset)
217 pos.moveTo(begin);
218 else
219 pos.moveTo(beginLine, beginOffset + offset - endOffset);
220 return true;
221 }
222 if (pos.lineNumber() > begin.lineNumber() && pos.lineNumber() < end.lineNumber()) {
223 pos.moveTo(begin);
224 return true;
225 }
226 return false;
227 }
228
229 private void adjustMarkers()
230 {
231 if (Editor.getEditorCount() > 1) {
232 for (EditorIterator it = new EditorIterator(); it.hasNext();) {
233 Editor ed = it.nextEditor();
234 if (ed == Editor.currentEditor())
235 continue;
236 if (ed.getBuffer() == buffer) {
237 if (adjustMarker(ed.getDot()))
239 ed.moveCaretToDotCol();
240 if (adjustMarker(ed.getMark()))
241 ed.setMark(null); Position top = new Position(ed.getTopLine(), 0);
243 if (adjustMarker(top)) {
244 ed.setTopLine(top.getLine());
245 ed.setUpdateFlag(REPAINT);
246 }
247 } else {
248 View view = (View) ed.views.get(buffer);
250 if (view != null) {
251 adjustMarker(view.dot);
252 if (adjustMarker(view.mark))
253 view.mark = null;
254 if (view.topLine != null) {
255 Position top = new Position(view.topLine, 0);
256 if (adjustMarker(top))
257 view.topLine = top.getLine();
258 }
259 }
260 }
261 }
262 }
263 List markers = Marker.getAllMarkers();
264 for (int i = markers.size(); i-- > 0;) {
265 Marker m = (Marker) markers.get(i);
266 if (m != null && m.getBuffer() == buffer)
267 adjustMarker(m.getPosition());
268 }
269 }
270
271 public void delete()
272 {
273 adjustMarkers();
274 try {
275 buffer.lockWrite();
276 }
277 catch (InterruptedException e) {
278 Log.error(e);
279 return;
280 }
281 try {
282 final String head = beginLine.substring(0, beginOffset);
283 final String tail = endLine.substring(endOffset);
284 if (beginLine == endLine) {
285 beginLine.setText(head.concat(tail));
286 } else {
287 FastStringBuffer sb = new FastStringBuffer();
288 for (Line line = beginLine; line != null; line = line.next()) {
289 if (line != endLine && !line.isNew()) {
291 if (sb.length() > 0)
292 sb.append('\n');
293 String s = line.getOriginalText();
294 sb.append(s != null ? s : line.getText());
295 } else if (line == endLine) {
296 if (!line.isNew()) {
297 if (sb.length() > 0)
298 sb.append('\n');
299 String s = line.getOriginalText();
300 sb.append(s != null ? s : line.getText());
301 }
302 break;
303 }
304 }
305 beginLine.setText(head.concat(tail));
306 beginLine.setOriginalText(sb.toString());
307 if (beginLine.isNew()) {
309 if (beginLine.getText().equals(beginLine.getOriginalText())) {
310 beginLine.setNew(false);
311 beginLine.setOriginalText(null);
312 }
313 }
314 Line nextLine = endLine.next();
315 beginLine.setNext(nextLine);
316 if (nextLine != null)
317 nextLine.setPrevious(beginLine);
318 buffer.needsRenumbering = true;
319 }
320 buffer.modified();
321 }
322 finally {
323 buffer.unlockWrite();
324 }
325 }
326 }
327 |
Popular Tags |
Java API By Example, From Geeks To Geeks.