KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > org > armedbear > j > UndoFold


1 /*
2  * UndoFold.java
3  *
4  * Copyright (C) 2002 Peter Graves
5  * $Id: UndoFold.java,v 1.1.1.1 2002/09/24 16:09:33 piso Exp $
6  *
7  * This program is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * 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 JavaDoc;
25 import javax.swing.undo.UndoableEdit JavaDoc;
26
27 public final class UndoFold extends AbstractUndoableEdit JavaDoc
28     implements Constants, UndoableEdit JavaDoc
29 {
30     private final State preState;
31     private State postState;
32
33     public UndoFold(Editor editor)
34     {
35         preState = new State(editor);
36     }
37
38     public void undo()
39     {
40         super.undo();
41         final Editor editor = Editor.currentEditor();
42         postState = new State(editor);
43         preState.restoreState(editor);
44         editor.setUpdateFlag(REFRAME);
45     }
46
47     public void redo()
48     {
49         super.redo();
50         final Editor editor = Editor.currentEditor();
51         postState.restoreState(editor);
52         editor.setUpdateFlag(REFRAME);
53     }
54
55     private static class State
56     {
57         final int dotLineNumber;
58         final int dotOffset;
59         final int markLineNumber;
60         final int markOffset;
61         final int absCaretCol;
62         final boolean isColumnSelection;
63         final HiddenLines hiddenLines;
64
65         State(Editor editor)
66         {
67             dotLineNumber = editor.getDotLine().lineNumber();;
68             dotOffset = editor.getDotOffset();
69             Position mark = editor.getMark();
70             if (mark != null) {
71                 markLineNumber = mark.lineNumber();
72                 markOffset = mark.getOffset();
73             } else {
74                 markLineNumber = -1;
75                 markOffset = -1;
76             }
77             absCaretCol = editor.getAbsoluteCaretCol();
78             isColumnSelection = editor.isColumnSelection();
79             hiddenLines = new HiddenLines(editor);
80         }
81
82         void restoreState(Editor editor)
83         {
84             // Remember the top line in the current edit window (try not to
85
// reframe unnecessarily).
86
final Display display = editor.getDisplay();
87             int topLineNumber = display.getTopLineNumber();
88
89             hiddenLines.restore();
90
91             // Use same top line if possible.
92
Line topLine = display.getTopLine();
93
94             if (topLine.isHidden()) {
95                 Line line = topLine.previousVisible();
96                 if (line == null)
97                     line = topLine.nextVisible();
98                 editor.setTopLine(line);
99             }
100             editor.setDot(dotLineNumber, dotOffset);
101             if (markLineNumber >= 0) {
102                 editor.setMark(markLineNumber, markOffset);
103                 editor.setColumnSelection(isColumnSelection);
104             } else
105                 editor.setMark(null);
106             display.setCaretCol(absCaretCol - display.getShift());
107             display.setUpdateFlag(REPAINT);
108
109             // Update any other windows displaying this buffer.
110
if (Editor.getEditorCount() > 1) {
111                 for (EditorIterator it = new EditorIterator(); it.hasNext();) {
112                     Editor ed = it.nextEditor();
113                     if (ed.getBuffer() == editor.getBuffer()) {
114                         // Make sure dot is visible.
115
if (ed.getDot().isHidden()) {
116                             Line line = ed.getDotLine().previousVisible();
117                             if (line != null) {
118                                 ed.setDot(line, 0);
119                                 ed.moveCaretToDotCol();
120                             }
121                         }
122                         ed.getDisplay().repaint();
123                     }
124                 }
125             }
126         }
127     }
128 }
129
Popular Tags