1 21 22 package org.armedbear.j; 23 24 import javax.swing.undo.AbstractUndoableEdit ; 25 import javax.swing.undo.UndoableEdit ; 26 27 public final class UndoFold extends AbstractUndoableEdit 28 implements Constants, UndoableEdit 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 final Display display = editor.getDisplay(); 87 int topLineNumber = display.getTopLineNumber(); 88 89 hiddenLines.restore(); 90 91 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 if (Editor.getEditorCount() > 1) { 111 for (EditorIterator it = new EditorIterator(); it.hasNext();) { 112 Editor ed = it.nextEditor(); 113 if (ed.getBuffer() == editor.getBuffer()) { 114 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 |