01: /*
02: * UndoMove.java
03: *
04: * Copyright (C) 2002-2003 Peter Graves
05: * $Id: UndoMove.java,v 1.2 2003/08/01 17:23:39 piso Exp $
06: *
07: * This program is free software; you can redistribute it and/or
08: * modify it under the terms of the GNU General Public License
09: * as published by the Free Software Foundation; either version 2
10: * of the License, or (at your option) any later version.
11: *
12: * This program is distributed in the hope that it will be useful,
13: * but WITHOUT ANY WARRANTY; without even the implied warranty of
14: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15: * GNU General Public License for more details.
16: *
17: * You should have received a copy of the GNU General Public License
18: * along with this program; if not, write to the Free Software
19: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
20: */
21:
22: package org.armedbear.j;
23:
24: import javax.swing.undo.AbstractUndoableEdit;
25:
26: public class UndoMove extends AbstractUndoableEdit implements Constants {
27: private final State preState;
28: private State postState;
29:
30: public UndoMove(Editor editor) {
31: preState = new State(editor);
32: }
33:
34: public void undo() {
35: super .undo();
36: final Editor editor = Editor.currentEditor();
37: postState = new State(editor);
38: preState.restoreState(editor);
39: editor.setUpdateFlag(REFRAME);
40: }
41:
42: public void redo() {
43: super .redo();
44: final Editor editor = Editor.currentEditor();
45: postState.restoreState(editor);
46: editor.setUpdateFlag(REFRAME);
47: }
48:
49: private static class State {
50: final int dotLineNumber;
51: final int dotOffset;
52: final int markLineNumber;
53: final int markOffset;
54: final int absCaretCol;
55: final boolean isColumnSelection;
56:
57: State(Editor editor) {
58: dotLineNumber = editor.getDotLine().lineNumber();
59: ;
60: dotOffset = editor.getDotOffset();
61: Position mark = editor.getMark();
62: if (mark != null) {
63: markLineNumber = mark.lineNumber();
64: markOffset = mark.getOffset();
65: } else {
66: markLineNumber = -1;
67: markOffset = -1;
68: }
69: absCaretCol = editor.getAbsoluteCaretCol();
70: isColumnSelection = editor.isColumnSelection();
71: }
72:
73: void restoreState(Editor editor) {
74: boolean wasMarked = editor.getMark() != null;
75: editor.updateDotLine();
76: editor.setDot(dotLineNumber, dotOffset);
77: if (markLineNumber >= 0) {
78: editor.setMark(markLineNumber, markOffset);
79: editor.setColumnSelection(isColumnSelection);
80: } else
81: editor.setMark(null);
82: editor.updateDotLine();
83: final Display display = editor.getDisplay();
84: display.setCaretCol(absCaretCol - display.getShift());
85: if (wasMarked || editor.getMark() != null)
86: display.setUpdateFlag(REPAINT);
87: }
88: }
89: }
|