001: /*BEGIN_COPYRIGHT_BLOCK
002: *
003: * Copyright (c) 2001-2007, JavaPLT group at Rice University (javaplt@rice.edu)
004: * All rights reserved.
005: *
006: * Redistribution and use in source and binary forms, with or without
007: * modification, are permitted provided that the following conditions are met:
008: * * Redistributions of source code must retain the above copyright
009: * notice, this list of conditions and the following disclaimer.
010: * * Redistributions in binary form must reproduce the above copyright
011: * notice, this list of conditions and the following disclaimer in the
012: * documentation and/or other materials provided with the distribution.
013: * * Neither the names of DrJava, the JavaPLT group, Rice University, nor the
014: * names of its contributors may be used to endorse or promote products
015: * derived from this software without specific prior written permission.
016: *
017: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
018: * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
019: * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
020: * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
021: * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
022: * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
023: * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
024: * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
025: * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
026: * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
027: * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
028: *
029: * This software is Open Source Initiative approved Open Source Software.
030: * Open Source Initative Approved is a trademark of the Open Source Initiative.
031: *
032: * This file is part of DrJava. Download the current version of this project
033: * from http://www.drjava.org/ or http://sourceforge.net/projects/drjava/
034: *
035: * END_COPYRIGHT_BLOCK*/
036:
037: package edu.rice.cs.drjava.model.repl;
038:
039: import java.util.Vector;
040: import java.util.HashMap;
041: import edu.rice.cs.util.FileOps;
042: import edu.rice.cs.util.StringOps;
043: import edu.rice.cs.drjava.config.*;
044: import edu.rice.cs.drjava.DrJava;
045: import edu.rice.cs.drjava.model.*;
046: import edu.rice.cs.util.OperationCanceledException;
047:
048: import java.io.Serializable;
049: import java.io.IOException;
050: import java.io.File;
051: import java.io.OutputStreamWriter;
052: import java.io.OutputStream;
053: import java.io.BufferedWriter;
054:
055: /** History class that records what has been typed in the interactions pane. This class is not thread safe;
056: * it is only accessed from InteractionsDocument which takes responsibility for synchronization.
057: * @version $Id: History.java 4264 2007-11-15 01:33:48Z mgricken $
058: */
059: public class History implements OptionConstants, Serializable {
060:
061: public static final String INTERACTION_SEPARATOR = "//End of Interaction//";
062:
063: // Not final because it may be updated by config
064: private volatile int _maxSize;
065:
066: /** Version flag at the beginning of saved history file format
067: * If this is not present in a saved history, it is assumed to be the original format.
068: */
069: public static final String HISTORY_FORMAT_VERSION_2 = "// DrJava saved history v2"
070: + StringOps.EOL;
071:
072: private final Vector<String> _vector = new Vector<String>();
073: private volatile int _cursor = -1;
074:
075: /** A hashmap for edited entries in the history. */
076: private final HashMap<Integer, String> _editedEntries = new HashMap<Integer, String>();
077:
078: /** A placeholder for the current search string. */
079: private volatile String _currentSearchString = "";
080:
081: /** Constructor, so we can add a listener to the Config item being used. */
082: public History() {
083: this (DrJava.getConfig().getSetting(HISTORY_MAX_SIZE).intValue());
084: DrJava.getConfig().addOptionListener(HISTORY_MAX_SIZE,
085: historyOptionListener);
086: }
087:
088: /** Creates a new History with the given size. An option listener is not added for the config framework.
089: * @param maxSize Number of lines to remember in the history.
090: */
091: public History(int maxSize) {
092: // Sanity check on _maxSize
093: if (maxSize < 0)
094: maxSize = 0;
095: _maxSize = maxSize;
096: }
097:
098: /** Adds an item to the history and moves the cursor to point to the place after it.
099: * Note: Items are not inserted if they are empty. (This is in accordance with
100: * bug #522123, but in divergence from feature #522213 which originally excluded
101: * sequential duplicate entries from ever being stored.)
102: *
103: * Thus, to access the newly inserted item, you must movePrevious first.
104: */
105: public void add(String item) {
106: // for consistency in saved History files, WILL save sequential duplicate entries
107: if (item.trim().length() > 0) {
108: _vector.add(item);
109: // If adding the new element has filled _vector to beyond max
110: // capacity, spill the oldest element out of the History.
111: if (_vector.size() > _maxSize) {
112: _vector.remove(0);
113: }
114: moveEnd();
115: _editedEntries.clear();
116: }
117: }
118:
119: /**
120: * Returns the last element and removes it, or returns null if the history is empty.
121: * @return last element before it was removed, or null if history is empty
122: */
123: public String removeLast() {
124: if (_vector.size() == 0) {
125: return null;
126: }
127: String last = _vector.remove(_vector.size() - 1);
128: if (_cursor > _vector.size()) {
129: _cursor = _vector.size() - 1;
130: }
131: return last;
132: }
133:
134: /** Move the cursor to just past the end. Thus, to access the last element, you must movePrevious. */
135: public void moveEnd() {
136: _cursor = _vector.size();
137: }
138:
139: /** Moves cursor back 1, or throws exception if there is none.
140: * @param entry the current entry (perhaps edited from what is in history)
141: */
142: public void movePrevious(String entry) {
143: if (!hasPrevious())
144: throw new ArrayIndexOutOfBoundsException();
145: setEditedEntry(entry);
146: _cursor--;
147: }
148:
149: /** Returns the last entry from the history. Throw array indexing exception if no such entry. */
150: public String lastEntry() {
151: return _vector.get(_cursor - 1);
152: }
153:
154: /** Moves cursor forward 1, or throws exception if there is none.
155: * @param entry the current entry (perhaps edited from what is in history)
156: */
157: public void moveNext(String entry) {
158: if (!hasNext())
159: throw new ArrayIndexOutOfBoundsException();
160: setEditedEntry(entry);
161: _cursor++;
162: }
163:
164: /** Returns whether moveNext() would succeed right now. */
165: public boolean hasNext() {
166: return _cursor < (_vector.size());
167: }
168:
169: /** Returns whether movePrevious() would succeed right now. */
170: public boolean hasPrevious() {
171: return _cursor > 0;
172: }
173:
174: /** Returns item in history at current position; returns "" if no current item exists. */
175: public String getCurrent() {
176: Integer cursor = new Integer(_cursor);
177: if (_editedEntries.containsKey(cursor))
178: return _editedEntries.get(cursor);
179:
180: if (hasNext())
181: return _vector.get(_cursor);
182: return "";
183: }
184:
185: /** Returns the number of items in this History. */
186: public int size() {
187: return _vector.size();
188: }
189:
190: /** Clears the vector */
191: public void clear() {
192: _vector.clear();
193: }
194:
195: /** Returns the history as a string by concatenating each string in the vector separated by the delimiting
196: * character. A semicolon is added to the end of every statement that didn't already end with one.
197: */
198: public String getHistoryAsStringWithSemicolons() {
199: final StringBuilder s = new StringBuilder();
200: final String delimiter = INTERACTION_SEPARATOR + StringOps.EOL;
201: for (int i = 0; i < _vector.size(); i++) {
202: String nextLine = _vector.get(i);
203: // int nextLength = nextLine.length();
204: // if ((nextLength > 0) && (nextLine.charAt(nextLength-1) != ';')) {
205: // nextLine += ";";
206: // }
207: // s += nextLine + delimiter;
208: s.append(nextLine);
209: s.append(delimiter);
210: }
211: return s.toString();
212: }
213:
214: /** Returns the history as a string by concatenating each string in the vector separated by the delimiting
215: * character.
216: */
217: public String getHistoryAsString() {
218: final StringBuilder sb = new StringBuilder();
219: final String delimiter = StringOps.EOL;
220: for (String s : _vector)
221: sb.append(s).append(delimiter);
222: return sb.toString();
223: }
224:
225: /** Writes this (unedited) History to the file selected in the FileSaveSelector.
226: * @param selector File to save to
227: */
228: public void writeToFile(FileSaveSelector selector)
229: throws IOException {
230: writeToFile(selector, getHistoryAsStringWithSemicolons());
231: }
232:
233: /** Writes this History to the file selected in the FileSaveSelector. The saved file will still include
234: * any tags or extensions needed to recognize it as a saved interactions file.
235: * @param selector File to save to
236: * @param editedVersion The edited version of the text to be saved.
237: */
238: public static void writeToFile(FileSaveSelector selector,
239: final String editedVersion) throws IOException {
240: File c;
241:
242: try {
243: c = selector.getFile();
244: } catch (OperationCanceledException oce) {
245: return;
246: }
247:
248: // Make sure we ask before overwriting
249: if (c != null) {
250: if (!c.exists() || selector.verifyOverwrite()) {
251: FileOps.DefaultFileSaver saver = new FileOps.DefaultFileSaver(
252: c) {
253: public void saveTo(OutputStream os)
254: throws IOException {
255:
256: OutputStreamWriter osw = new OutputStreamWriter(
257: os);
258: BufferedWriter bw = new BufferedWriter(osw);
259: String file = HISTORY_FORMAT_VERSION_2
260: + editedVersion;
261: // if (PlatformFactory.ONLY.isWindowsPlatform()) {
262: // StringBuffer buf = new StringBuffer();
263: // String lineSep = StringOps.EOL;
264: // int last = 0;
265: // for (int i = file.indexOf('\n'); i != -1; i = file.indexOf('\n', last)) {
266: // buf.append(file.substring(last, i));
267: // buf.append(lineSep);
268: // last = i+1;
269: // }
270: // file = buf.toString();
271: // }
272: bw.write(file, 0, file.length());
273: bw.close();
274: }
275: };
276: FileOps.saveFile(saver);
277: }
278: }
279: }
280:
281: /** Changes the maximum number of interactions remembered by this History.
282: * @param newSize New number of interactions to remember.
283: */
284: public void setMaxSize(int newSize) {
285: // Sanity check
286: if (newSize < 0)
287: newSize = 0;
288:
289: // Remove old elements if the new size is less than current size
290: if (size() > newSize) {
291:
292: int numToDelete = size() - newSize;
293:
294: for (int i = 0; i < numToDelete; i++) {
295: _vector.remove(0);
296: }
297:
298: moveEnd();
299: }
300: _maxSize = newSize;
301: }
302:
303: /** The OptionListener for HISTORY_MAX_SIZE */
304: public final OptionListener<Integer> historyOptionListener = new OptionListener<Integer>() {
305: public void optionChanged(OptionEvent<Integer> oce) {
306: int newSize = oce.value.intValue();
307: setMaxSize(newSize);
308: }
309: };
310:
311: /* Getter for historyOptionListener. */
312: public OptionListener<Integer> getHistoryOptionListener() {
313: return historyOptionListener;
314: }
315:
316: /** Sets the edited entry to the given value.
317: * @param entry the string to set
318: */
319: public void setEditedEntry(String entry) {
320: if (!entry.equals(getCurrent()))
321: _editedEntries.put(new Integer(_cursor), entry);
322: }
323:
324: /** Reverse-searches the history for the previous matching string.
325: * @param currentInteraction the current interaction
326: */
327: public void reverseSearch(String currentInteraction) {
328: if (_currentSearchString.equals("")
329: || !currentInteraction.startsWith(_currentSearchString))
330: _currentSearchString = currentInteraction;
331:
332: setEditedEntry(currentInteraction);
333: while (hasPrevious()) {
334: movePrevious(getCurrent());
335: if (getCurrent().startsWith(_currentSearchString, 0))
336: break;
337: }
338:
339: if (!getCurrent().startsWith(_currentSearchString, 0))
340: moveEnd();
341: }
342:
343: /** Forward-searches the history for the next matching string.
344: * @param currentInteraction the current interaction
345: */
346: public void forwardSearch(String currentInteraction) {
347: if (_currentSearchString.equals("")
348: || !currentInteraction.startsWith(_currentSearchString))
349: _currentSearchString = currentInteraction;
350:
351: setEditedEntry(currentInteraction);
352: while (hasNext()) {
353: moveNext(getCurrent());
354: if (getCurrent().startsWith(_currentSearchString, 0))
355: break;
356: }
357:
358: if (!getCurrent().startsWith(_currentSearchString, 0))
359: moveEnd();
360: }
361: }
|