001: /*
002: * UndoManager.java - Buffer undo manager
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 2001, 2005 Slava Pestov
007: *
008: * This program is free software; you can redistribute it and/or
009: * modify it under the terms of the GNU General Public License
010: * as published by the Free Software Foundation; either version 2
011: * of the License, or any later version.
012: *
013: * This program is distributed in the hope that it will be useful,
014: * but WITHOUT ANY WARRANTY; without even the implied warranty of
015: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
016: * GNU General Public License for more details.
017: *
018: * You should have received a copy of the GNU General Public License
019: * along with this program; if not, write to the Free Software
020: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
021: */
022:
023: package org.gjt.sp.jedit.buffer;
024:
025: //{{{ Imports
026: import org.gjt.sp.jedit.jEdit;
027: import org.gjt.sp.util.Log;
028:
029: //}}}
030:
031: /**
032: * A class internal to jEdit's document model. You should not use it
033: * directly. To improve performance, none of the methods in this class
034: * check for out of bounds access, nor are they thread-safe. The
035: * <code>Buffer</code> class, through which these methods must be
036: * called through, implements such protection.
037: *
038: * @author Slava Pestov
039: * @version $Id: UndoManager.java 9059 2007-03-02 05:24:57Z vanza $
040: * @since jEdit 4.0pre1
041: */
042: public class UndoManager {
043: //{{{ UndoManager constructor
044: public UndoManager(JEditBuffer buffer) {
045: this .buffer = buffer;
046: } //}}}
047:
048: //{{{ setLimit() method
049: public void setLimit(int limit) {
050: this .limit = limit;
051: } //}}}
052:
053: //{{{ clear() method
054: public void clear() {
055: undosFirst = undosLast = redosFirst = redosLast = null;
056: undoCount = 0;
057: } //}}}
058:
059: //{{{ undo() method
060: public int undo() {
061: if (insideCompoundEdit())
062: throw new InternalError(
063: "Unbalanced begin/endCompoundEdit()");
064:
065: if (undosLast == null)
066: return -1;
067: else {
068: undoCount--;
069:
070: int caret = undosLast.undo();
071: redosFirst = undosLast;
072: undosLast = undosLast.prev;
073: if (undosLast == null)
074: undosFirst = null;
075: return caret;
076: }
077: } //}}}
078:
079: //{{{ redo() method
080: public int redo() {
081: if (insideCompoundEdit())
082: throw new InternalError(
083: "Unbalanced begin/endCompoundEdit()");
084:
085: if (redosFirst == null)
086: return -1;
087: else {
088: undoCount++;
089:
090: int caret = redosFirst.redo();
091: undosLast = redosFirst;
092: if (undosFirst == null)
093: undosFirst = undosLast;
094: redosFirst = redosFirst.next;
095: return caret;
096: }
097: } //}}}
098:
099: //{{{ beginCompoundEdit() method
100: public void beginCompoundEdit() {
101: if (compoundEditCount == 0)
102: compoundEdit = new CompoundEdit();
103:
104: compoundEditCount++;
105: } //}}}
106:
107: //{{{ endCompoundEdit() method
108: public void endCompoundEdit() {
109: if (compoundEditCount == 0) {
110: Log.log(Log.WARNING, this , new Exception(
111: "Unbalanced begin/endCompoundEdit()"));
112: return;
113: } else if (compoundEditCount == 1) {
114: if (compoundEdit.first == null)
115: /* nothing done between begin/end calls */;
116: else if (compoundEdit.first == compoundEdit.last)
117: addEdit(compoundEdit.first);
118: else
119: addEdit(compoundEdit);
120:
121: compoundEdit = null;
122: }
123:
124: compoundEditCount--;
125: } //}}}
126:
127: //{{{ insideCompoundEdit() method
128: public boolean insideCompoundEdit() {
129: return compoundEditCount != 0;
130: } //}}}
131:
132: //{{{ contentInserted() method
133: public void contentInserted(int offset, int length, String text,
134: boolean clearDirty) {
135: Edit last = getLastEdit();
136: Edit toMerge = getMergeEdit();
137:
138: if (!clearDirty && toMerge instanceof Insert
139: && redosFirst == null) {
140: Insert ins = (Insert) toMerge;
141: if (ins.offset == offset) {
142: ins.str = text.concat(ins.str);
143: ins.length += length;
144: return;
145: } else if (ins.offset + ins.length == offset) {
146: ins.str = ins.str.concat(text);
147: ins.length += length;
148: return;
149: }
150: }
151:
152: Insert ins = new Insert(this , offset, length, text);
153:
154: if (clearDirty) {
155: redoClearDirty = last;
156: undoClearDirty = ins;
157: }
158:
159: if (compoundEdit != null)
160: compoundEdit.add(ins);
161: else
162: addEdit(ins);
163: } //}}}
164:
165: //{{{ contentRemoved() method
166: public void contentRemoved(int offset, int length, String text,
167: boolean clearDirty) {
168: Edit last = getLastEdit();
169: Edit toMerge = getMergeEdit();
170:
171: if (!clearDirty && toMerge instanceof Remove
172: && redosFirst == null) {
173: Remove rem = (Remove) toMerge;
174: if (rem.offset == offset) {
175: rem.str = rem.str.concat(text);
176: rem.hashcode = rem.str.hashCode();
177: rem.length += length;
178: KillRing.getInstance().changed(rem);
179: return;
180: } else if (offset + length == rem.offset) {
181: rem.str = text.concat(rem.str);
182: rem.hashcode = rem.str.hashCode();
183: rem.length += length;
184: rem.offset = offset;
185: KillRing.getInstance().changed(rem);
186: return;
187: }
188: }
189:
190: Remove rem = new Remove(this , offset, length, text);
191: if (clearDirty) {
192: redoClearDirty = last;
193: undoClearDirty = rem;
194: }
195:
196: if (compoundEdit != null)
197: compoundEdit.add(rem);
198: else
199: addEdit(rem);
200:
201: KillRing.getInstance().add(rem);
202: } //}}}
203:
204: //{{{ bufferSaved() method
205: public void bufferSaved() {
206: if (jEdit.getBooleanProperty("resetUndoOnSave")) {
207: clear();
208: } else {
209: resetClearDirty();
210: }
211:
212: } //}}}
213:
214: //{{{ resetClearDirty method
215: public void resetClearDirty() {
216: redoClearDirty = getLastEdit();
217: if (redosFirst instanceof CompoundEdit)
218: undoClearDirty = ((CompoundEdit) redosFirst).first;
219: else
220: undoClearDirty = redosFirst;
221: } //}}}
222:
223: //{{{ Private members
224:
225: //{{{ Instance variables
226: private JEditBuffer buffer;
227:
228: // queue of undos. last is most recent, first is oldest
229: private Edit undosFirst;
230: private Edit undosLast;
231:
232: // queue of redos. first is most recent, last is oldest
233: private Edit redosFirst;
234: private Edit redosLast;
235:
236: private int limit;
237: private int undoCount;
238: private int compoundEditCount;
239: private CompoundEdit compoundEdit;
240: private Edit undoClearDirty, redoClearDirty;
241:
242: //}}}
243:
244: //{{{ addEdit() method
245: private void addEdit(Edit edit) {
246: if (undosFirst == null)
247: undosFirst = undosLast = edit;
248: else {
249: undosLast.next = edit;
250: edit.prev = undosLast;
251: undosLast = edit;
252: }
253:
254: redosFirst = redosLast = null;
255:
256: undoCount++;
257:
258: while (undoCount > limit) {
259: undoCount--;
260:
261: if (undosFirst == undosLast)
262: undosFirst = undosLast = null;
263: else {
264: undosFirst.next.prev = null;
265: undosFirst = undosFirst.next;
266: }
267: }
268: } //}}}
269:
270: //{{{ getMergeEdit() method
271: private Edit getMergeEdit() {
272: Edit last = getLastEdit();
273: return (compoundEdit != null ? compoundEdit.last : last);
274: } //}}}
275:
276: //{{{ getLastEdit() method
277: private Edit getLastEdit() {
278: if (undosLast instanceof CompoundEdit)
279: return ((CompoundEdit) undosLast).last;
280: else
281: return undosLast;
282: } //}}}
283:
284: //}}}
285:
286: //{{{ Inner classes
287:
288: //{{{ Edit class
289: abstract static class Edit {
290: Edit prev, next;
291:
292: //{{{ undo() method
293: abstract int undo();
294:
295: //}}}
296:
297: //{{{ redo() method
298: abstract int redo();
299: //}}}
300: } //}}}
301:
302: //{{{ Insert class
303: static class Insert extends Edit {
304: //{{{ Insert constructor
305: Insert(UndoManager mgr, int offset, int length, String str) {
306: this .mgr = mgr;
307: this .offset = offset;
308: this .length = length;
309: this .str = str;
310: } //}}}
311:
312: //{{{ undo() method
313: int undo() {
314: mgr.buffer.remove(offset, length);
315: if (mgr.undoClearDirty == this )
316: mgr.buffer.setDirty(false);
317: return offset;
318: } //}}}
319:
320: //{{{ redo() method
321: int redo() {
322: mgr.buffer.insert(offset, str);
323: if (mgr.redoClearDirty == this )
324: mgr.buffer.setDirty(false);
325: return offset + length;
326: } //}}}
327:
328: UndoManager mgr;
329: int offset;
330: int length;
331: String str;
332: } //}}}
333:
334: //{{{ Remove class
335: public static class Remove extends Edit {
336: //{{{ Remove constructor
337: Remove(UndoManager mgr, int offset, int length, String str) {
338: this .mgr = mgr;
339: this .offset = offset;
340: this .length = length;
341: this .str = str;
342: hashcode = str.hashCode();
343: } //}}}
344:
345: //{{{ undo() method
346: int undo() {
347: mgr.buffer.insert(offset, str);
348: if (mgr.undoClearDirty == this )
349: mgr.buffer.setDirty(false);
350: return offset + length;
351: } //}}}
352:
353: //{{{ redo() method
354: int redo() {
355: mgr.buffer.remove(offset, length);
356: if (mgr.redoClearDirty == this )
357: mgr.buffer.setDirty(false);
358: return offset;
359: } //}}}
360:
361: //{{{ toString() method
362: public String toString() {
363: return str;
364: } //}}}
365:
366: UndoManager mgr;
367: int offset;
368: int length;
369: String str;
370: int hashcode;
371: boolean inKillRing;
372: } //}}}
373:
374: //{{{ CompoundEdit class
375: static class CompoundEdit extends Edit {
376: //{{{ undo() method
377: public int undo() {
378: int retVal = -1;
379: Edit edit = last;
380: while (edit != null) {
381: retVal = edit.undo();
382: edit = edit.prev;
383: }
384: return retVal;
385: } //}}}
386:
387: //{{{ redo() method
388: public int redo() {
389: int retVal = -1;
390: Edit edit = first;
391: while (edit != null) {
392: retVal = edit.redo();
393: edit = edit.next;
394: }
395: return retVal;
396: } //}}}
397:
398: //{{{ add() method
399: public void add(Edit edit) {
400: if (first == null)
401: first = last = edit;
402: else {
403: edit.prev = last;
404: last.next = edit;
405: last = edit;
406: }
407: } //}}}
408:
409: Edit first, last;
410: } //}}}
411:
412: //}}}
413: }
|