|
1
21
22 package org.armedbear.j;
23
24 import javax.swing.undo.AbstractUndoableEdit  ;
25 import javax.swing.undo.UndoableEdit ;
26
27 public class UndoLineEdit extends AbstractUndoableEdit implements Constants,
28 UndoableEdit
29 {
30 private final Buffer buffer;
31 private final int changeLineNumber;
32 private final State preState;
33 private State postState;
34
35 public UndoLineEdit(Editor editor)
36 {
37 buffer = editor.getBuffer();
38 changeLineNumber = editor.getDot().lineNumber();
39 preState = new State(editor);
40 }
41
42 public UndoLineEdit(Buffer buffer, Line line)
43 {
44 this.buffer = buffer;
45 changeLineNumber = line.lineNumber();
46 preState = new State(buffer);
47 }
48
49 public boolean addEdit(UndoableEdit edit)
50 {
51 if (edit instanceof UndoLineEdit) {
52 UndoLineEdit e = (UndoLineEdit) edit;
53 if (e.changeLineNumber == this.changeLineNumber)
54 return true;
55 }
56 return false;
57 }
58
59 public void undo()
60 {
61 super.undo();
62 final Editor editor = Editor.currentEditor();
63 Debug.assertTrue(editor.getBuffer() == buffer);
64 postState = new State(editor);
65 preState.restoreState(editor);
66 editor.setUpdateFlag(REFRAME);
67
68 if (postState.modificationCount != preState.modificationCount) {
69 buffer.invalidate();
71 Sidebar.setUpdateFlagInAllFrames(SIDEBAR_MODIFIED_BUFFER_COUNT |
72 SIDEBAR_REPAINT_BUFFER_LIST);
73 Sidebar.repaintBufferListInAllFrames();
74 }
75 }
76
77 public void redo()
78 {
79 super.redo();
80 final Editor editor = Editor.currentEditor();
81 Debug.assertTrue(editor.getBuffer() == buffer);
82 postState.restoreState(editor);
83 editor.setUpdateFlag(REFRAME);
84
85 if (postState.modificationCount != preState.modificationCount) {
86 buffer.invalidate();
88 Sidebar.setUpdateFlagInAllFrames(SIDEBAR_MODIFIED_BUFFER_COUNT |
89 SIDEBAR_REPAINT_BUFFER_LIST);
90 Sidebar.repaintBufferListInAllFrames();
91 }
92 }
93
94 private class State
95 {
96 final int dotLineNumber;
97 final int dotOffset;
98 final int markLineNumber;
99 final int markOffset;
100 final int absCaretCol;
101 final boolean isColumnSelection;
102 final int modificationCount;
103 final boolean modified;
104 final Line line;
105
106 State(Editor editor)
107 {
108 final Line dotLine = editor.getDotLine();
109 dotLineNumber = dotLine.lineNumber();
110 final int length = dotLine.length();
111 final int offset = editor.getDotOffset();
112 if (offset > length)
113 Debug.bug();
114 dotOffset = offset > length ? length : offset;
115 absCaretCol = editor.getAbsoluteCaretCol();
116 Position mark = editor.getMark();
117 if (mark != null) {
118 markLineNumber = mark.lineNumber();
119 markOffset = mark.getOffset();
120 } else {
121 markLineNumber = -1;
122 markOffset = -1;
123 }
124 isColumnSelection = editor.isColumnSelection();
125 final Buffer buffer = editor.getBuffer();
126 modificationCount = buffer.getModCount();
127 modified = buffer.isModified();
128 line = buffer.getLine(changeLineNumber).copy();
129 }
130
131 State(Buffer buffer)
132 {
133 dotLineNumber = -1;
134 dotOffset = -1;
135 absCaretCol = -1;
136 markLineNumber = -1;
137 markOffset = -1;
138 isColumnSelection = false;
139 modificationCount = buffer.getModCount();
140 modified = buffer.isModified();
141 line = buffer.getLine(changeLineNumber).copy();
142 }
143
144 void restoreState(Editor editor)
145 {
146 Debug.assertTrue(editor.getBuffer() == buffer);
147 Debug.assertTrue(changeLineNumber >= 0);
148
149 if (!buffer.isWriteLocked())
150 Debug.bug();
151 Line changeLine = buffer.getLine(changeLineNumber);
152 changeLine.copy(line);
153 Editor.updateInAllEditors(changeLine);
154
155 buffer.setModCount(modificationCount);
156
157 boolean wasMarked = editor.getMark() != null;
158 editor.updateDotLine();
159 editor.setDot(dotLineNumber, dotOffset);
160 if (dotOffset > editor.getDotLine().length()) {
161 Debug.bug();
162 editor.getDot().setOffset(editor.getDotLine().length());
163 }
164 if (markLineNumber >= 0) {
165 editor.setMark(markLineNumber, markOffset);
166 editor.setColumnSelection(isColumnSelection);
167 } else
168 editor.setMark(null);
169 editor.updateDotLine();
170 final Display display = editor.getDisplay();
171 if (absCaretCol >= 0)
172 display.setCaretCol(absCaretCol - display.getShift());
173 if (wasMarked || editor.getMark() != null)
174 display.setUpdateFlag(REPAINT);
175 }
176 }
177 }
178 |
Popular Tags |
Java API By Example, From Geeks To Geeks.