001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.gui.nodeviews;
009:
010: import java.awt.Color;
011: import java.awt.event.FocusEvent;
012: import java.awt.event.FocusListener;
013: import java.awt.event.KeyEvent;
014: import java.awt.event.KeyListener;
015: import java.util.regex.Matcher;
016: import java.util.regex.Pattern;
017: import java.util.regex.PatternSyntaxException;
018:
019: import javax.swing.JComponent;
020:
021: import de.uka.ilkd.key.gui.Main;
022: import de.uka.ilkd.key.pp.Range;
023:
024: /**
025: * Implements an incremental search for the sequent view. The incremental search
026: * starts with <code>/</code> and is aborted if the sequent view looses the
027: * focus or the key <code>Esc</code> is pressed. The next match can be found
028: * pressing the function key <code>F3</code>.
029: *
030: */
031: public class IncrementalSearch implements KeyListener, FocusListener {
032:
033: private int startPos;
034:
035: private String searchStr;
036:
037: private Object searchHighlight;
038:
039: private SequentView seqView;
040:
041: private Main main;
042:
043: /**
044: * create and initialize a new incremental search run
045: *
046: * @param seqView
047: * the SequentView where to perform an incremental search
048: */
049: public IncrementalSearch(SequentView seqView) {
050:
051: if (alreadyRegistered(seqView)) {
052: return;
053: }
054:
055: this .seqView = seqView;
056:
057: init();
058:
059: if (seqView.mediator().mainFrame() instanceof Main) {
060: main = (Main) seqView.mediator().mainFrame();
061: }
062:
063: printStatus("Search: " + searchStr);
064:
065: }
066:
067: /**
068: * checks if an incremental search is already taken place at the specified
069: * sequent view
070: *
071: * @param comp
072: * the JComponent to be checked
073: * @return true if incremental search has been already activated for the
074: * component
075: */
076: private boolean alreadyRegistered(JComponent comp) {
077: KeyListener[] l = comp.getKeyListeners();
078: for (int i = 0; i < l.length; i++) {
079: if (l[i] instanceof IncrementalSearch) {
080: return true;
081: }
082: }
083: return false;
084: }
085:
086: /**
087: * initialises the incremental search
088: */
089: private void init() {
090: searchStr = "";
091: startPos = seqView.getCaret().getMark();
092: searchHighlight = seqView.getColorHighlight(Color.RED);
093:
094: seqView.addKeyListener(this );
095: seqView.addFocusListener(this );
096: }
097:
098: /**
099: * disable this searcher
100: */
101: private void disableSearchMode() {
102: seqView.removeKeyListener(this );
103: seqView.removeFocusListener(this );
104: seqView.removeHighlight(searchHighlight);
105:
106: searchStr = "";
107: startPos = 0;
108:
109: if (main != null) {
110: main.setStandardStatusLine();
111: }
112: }
113:
114: /**
115: * disables the incremental searcher when the function key <code>F3</code>
116: * is pressed
117: */
118: public void keyPressed(KeyEvent e) {
119: if (e.getKeyCode() == KeyEvent.VK_F3) {
120: startPos = startPos + 1;
121: seqView.setCaretPosition(startPos);
122: searchPattern();
123: }
124: }
125:
126: /**
127: * does nothing
128: */
129: public void keyReleased(KeyEvent e) {
130: }
131:
132: /**
133: * constructs the string to serach for
134: */
135: public void keyTyped(KeyEvent e) {
136: final char ch = e.getKeyChar();
137: switch (ch) {
138: case KeyEvent.VK_ESCAPE:
139: disableSearchMode();
140: return;
141: case KeyEvent.VK_BACK_SPACE:
142: if (searchStr.length() > 1) {
143: searchStr = searchStr.substring(0,
144: searchStr.length() - 1);
145: } else {
146: disableSearchMode();
147: return;
148: }
149: break;
150: default:
151: searchStr += ch;
152: break;
153: }
154: searchPattern();
155: }
156:
157: /**
158: * searches for the occurence of the specified string
159: */
160: private void searchPattern() {
161:
162: String escaped = searchStr
163: .replaceAll(
164: "([\\+ | \\* | \\| | \\\\ | \\[ | \\] | \\{ | \\} | \\( | \\)])",
165: "\\\\$1");
166:
167: seqView.disableHighlights();
168:
169: int caseInsensitiveFlag = 0;
170:
171: // no capital letters used --> case insensitive matching
172: if (searchStr.toLowerCase().equals(searchStr)) {
173: caseInsensitiveFlag = Pattern.CASE_INSENSITIVE;
174: }
175:
176: Pattern p;
177: try {
178: p = Pattern.compile(escaped, caseInsensitiveFlag);
179: } catch (PatternSyntaxException pse) {
180: return;
181: } catch (IllegalArgumentException iae) {
182: return;
183: }
184:
185: Matcher m = p.matcher(seqView.getText());
186:
187: String status = "Search: " + searchStr;
188:
189: if (m.find(startPos)) {
190: int foundAt = m.start();
191: startPos = foundAt;
192: seqView.setCaretPosition(foundAt);
193: seqView.paintHighlight(new Range(foundAt, foundAt
194: + searchStr.length()), searchHighlight);
195: } else {
196: startPos = 0;
197: status += " (not found)";
198: }
199:
200: printStatus(status);
201: }
202:
203: /**
204: * prints the given String in the statusline
205: */
206: private void printStatus(String text) {
207: if (main != null) {
208: main.setStatusLine(text);
209: }
210: }
211:
212: // the methods below implement the focus listener
213: // incremental search is aborted if the sequent view has no
214: // longer the focus
215:
216: public void focusGained(FocusEvent e) {
217:
218: }
219:
220: /**
221: * aborts incremental search, if the observed component looses the focus
222: */
223: public void focusLost(FocusEvent e) {
224: disableSearchMode();
225: seqView.removeFocusListener(this);
226: }
227: }
|