001: package snow.texteditor;
002:
003: import javax.swing.text.*;
004: import javax.swing.undo.*;
005: import javax.swing.event.*;
006: import java.awt.*;
007: import java.util.*;
008:
009: /** A document with an undo capability.
010: */
011: public class UndoableDocument extends SimpleDocument implements
012: UndoableEditListener {
013: /** UndoManager that we add edits to. */
014: private UndoManager undoManager_ = new UndoManager();
015:
016: private boolean doNotUndoThis = false;
017:
018: public UndoableDocument() {
019: addUndoableEditListener(this );
020: }
021:
022: /** Allow to retrieve the undo manager. Can be later readded
023: after the text has been repasted. Useful when simulating multiple documents in the same doc.
024: */
025: public final UndoManager getAndRemoveUndoManager() {
026: this .removeUndoableEditListener(this );
027: UndoManager um = undoManager_;
028: undoManager_ = null;
029: return um;
030: }
031:
032: public final void reinstallUndoManager(UndoManager um) {
033: if (undoManager_ != null) {
034: System.out.println("PROBLEM: undomanager not null");
035: this .removeUndoableEditListener(this );
036: }
037: this .undoManager_ = um;
038: this .addUndoableEditListener(this );
039: }
040:
041: //
042: // UNDO Manager interface
043: // he is not accessible from outside...
044: //
045:
046: public void _setUndoEnabled(boolean state) {
047: doNotUndoThis = state;
048: }
049:
050: // important: the styler really polls a lot of style calls that are not of interrest
051: // with this flag set to true, all style changes are ignored
052: public boolean ignoreStyleUndos = true;
053:
054: /**
055: * Messaged when the Document has created an edit, the edit is
056: * added to <code>undo</code>, an instance of UndoManager.
057: */
058: public void undoableEditHappened(UndoableEditEvent e) {
059: if (doNotUndoThis == false) {
060: if (ignoreStyleUndos) {
061: if (e.getEdit() instanceof AbstractDocument.DefaultDocumentEvent) {
062: AbstractDocument.DefaultDocumentEvent de = (AbstractDocument.DefaultDocumentEvent) e
063: .getEdit();
064: // this selects the style events, the others are INSERT or REMOVE
065: if (de.getType() == DocumentEvent.EventType.CHANGE) {
066: e.getEdit().die();
067: return;
068: }
069: }
070:
071: }
072: if (undoManager_ != null) {
073: undoManager_.addEdit(e.getEdit());
074: alertListenersThatUndoManagerStateChanged();
075: }
076: }
077: }
078:
079: public void undo() {
080: try {
081: if (undoManager_.canUndo()) {
082: undoManager_.undo();
083: alertListenersThatUndoManagerStateChanged();
084: }
085: } catch (Exception cue) {
086: // not only UndoExceptions....
087: cue.printStackTrace();
088: }
089: }
090:
091: public void redo() {
092: try {
093: if (undoManager_.canRedo()) {
094: undoManager_.redo();
095: alertListenersThatUndoManagerStateChanged();
096: }
097: } catch (Exception cue) {
098: cue.printStackTrace();
099: // not only UndoExceptions....
100: }
101: }
102:
103: public boolean canUndo() {
104: return undoManager_.canUndo();
105: }
106:
107: public boolean canRedo() {
108: return undoManager_.canRedo();
109: }
110:
111: public String getNextUndoName() {
112: return undoManager_.getUndoPresentationName();
113: }
114:
115: public String getNextRedoName() {
116: return undoManager_.getRedoPresentationName();
117: }
118:
119: public void deleteUndoBuffer() {
120: undoManager_.discardAllEdits();
121: alertListenersThatUndoManagerStateChanged();
122: }
123:
124: // Undo manager listener
125: //
126:
127: private final Vector<ChangeListener> undoManagerlisteners = new Vector<ChangeListener>();
128:
129: /**
130: * Allows one to listen to the undoManager state change,
131: * used for the undo/redo button visibilities.
132: */
133: public void addUndoManagerListener(ChangeListener listener) {
134: synchronized (undoManagerlisteners) {
135: undoManagerlisteners.addElement(listener);
136: }
137: }
138:
139: public void removeUndoManagerListener(ChangeListener listener) {
140: synchronized (undoManagerlisteners) {
141: undoManagerlisteners.removeElement(listener);
142: }
143: }
144:
145: private void alertListenersThatUndoManagerStateChanged() {
146: // make a copy to safely iterates. Avoid concurrent access problems
147: ChangeListener[] cls = null;
148: synchronized (undoManagerlisteners) {
149: cls = undoManagerlisteners
150: .toArray(new ChangeListener[undoManagerlisteners
151: .size()]);
152: }
153:
154: for (ChangeListener cl : cls) {
155: cl.stateChanged(new ChangeEvent(this ));
156: }
157: }
158:
159: public void terminate() {
160: this .removeUndoableEditListener(this );
161: // delete all references
162: undoManagerlisteners.removeAllElements();
163: undoManager_.discardAllEdits();
164: }
165:
166: }
|