edu.rice.cs.drjava.model.repl
Class History
java.lang.Object
|
+--edu.rice.cs.drjava.model.repl.History
- All Implemented Interfaces:
- OptionConstants
- public class History
- extends Object
- implements OptionConstants
Keeps track of what was typed in the interactions pane.
- Version:
- $Id: History.java,v 1.17 2002/09/02 21:24:12 csreis Exp $
Fields inherited from interface edu.rice.cs.drjava.config.OptionConstants |
COMPILER_ERROR_COLOR, DEBUG_BREAKPOINT_COLOR, DEBUG_SHOW_THREADS, DEBUG_SOURCEPATH, DEBUG_STEP_DRJAVA, DEBUG_STEP_INTERPRETER, DEBUG_STEP_JAVA, DEBUG_THREAD_COLOR, DEFINITIONS_BACKGROUND_COLOR, DEFINITIONS_COMMENT_COLOR, DEFINITIONS_DOUBLE_QUOTED_COLOR, DEFINITIONS_KEYWORD_COLOR, DEFINITIONS_MATCH_COLOR, DEFINITIONS_NORMAL_COLOR, DEFINITIONS_NUMBER_COLOR, DEFINITIONS_SINGLE_QUOTED_COLOR, DEFINITIONS_TYPE_COLOR, EXTRA_CLASSPATH, FONT_DOCLIST, FONT_MAIN, FONT_TOOLBAR, HISTORY_MAX_SIZE, INDENT_LEVEL, INTERACTIONS_EXIT_PROMPT, JAVAC_ALLOW_ASSERT, JAVAC_LOCATION, JSR14_COLLECTIONSPATH, JSR14_LOCATION, KEY_BACKWARD, KEY_BEGIN_DOCUMENT, KEY_BEGIN_LINE, KEY_CLOSE_FILE, KEY_COMPILE, KEY_COMPILE_ALL, KEY_COPY, KEY_CUT, KEY_CUT_LINE, KEY_DEBUG_BREAKPOINT_TOGGLE, KEY_DEBUG_MODE_TOGGLE, KEY_DEBUG_RESUME, KEY_DEBUG_STEP_INTO, KEY_DEBUG_STEP_OUT, KEY_DEBUG_STEP_OVER, KEY_DELETE_NEXT, KEY_DELETE_PREVIOUS, KEY_DOWN, KEY_END_DOCUMENT, KEY_END_LINE, KEY_FIND_NEXT, KEY_FIND_REPLACE, KEY_FORWARD, KEY_GOTO_LINE, KEY_NEW_FILE, KEY_NEXT_DOCUMENT, KEY_NEXT_WORD, KEY_OPEN_FILE, KEY_PAGE_DOWN, KEY_PAGE_UP, KEY_PASTE, KEY_PREVIOUS_DOCUMENT, KEY_PREVIOUS_WORD, KEY_PRINT, KEY_PRINT_PREVIEW, KEY_QUIT, KEY_REDO, KEY_SAVE_FILE, KEY_SAVE_FILE_AS, KEY_SELECT_ALL, KEY_UNDO, KEY_UP, LINEENUM_ENABLED, mask, QUIT_PROMPT, RECENT_FILES, RECENT_FILES_MAX_SIZE, TOOLBAR_ICONS_ENABLED, TOOLBAR_TEXT_ENABLED, WORKING_DIRECTORY |
Constructor Summary |
History()
Constructor, so we can add a listener to the Config item being used. |
Method Summary |
void |
add(String item)
Adds an item to the history and moves the cursor to point
to the place after it. |
void |
clear()
Clears the vector |
String |
getCurrent()
Returns item in history at current position, or throws exception if none. |
String |
getHistoryAsString()
Returns the history as a string by concatenating each string in the vector
separated by the delimiting character |
boolean |
hasNext()
Returns whether moveNext() would succeed right now. |
boolean |
hasPrevious()
Returns whether movePrevious() would succeed right now. |
void |
moveEnd()
Move the cursor to just past the end. |
void |
moveNext()
Moves cursor forward 1, or throws exception if there is none. |
void |
movePrevious()
Moves cursor back 1, or throws exception if there is none. |
int |
size()
Returns the number of items in this History. |
void |
writeToFile(FileSaveSelector selector)
Writes this History to a the file selected in the FileSaveSelector |
Methods inherited from class java.lang.Object |
, clone, equals, finalize, getClass, hashCode, notify, notifyAll, registerNatives, toString, wait, wait, wait |
MAX_SIZE
private static int MAX_SIZE
_vector
private gj.util.Vector _vector
_cursor
private int _cursor
History
public History()
- Constructor, so we can add a listener to the Config item being used.
add
public void add(String item)
- Adds an item to the history and moves the cursor to point
to the place after it.
Note: Items are not inserted if they are empty. (This is in accordance with
bug #522123, but in divergence from feature #522213 which originally excluded
sequential duplicate entries from ever being stored.)
Thus, to access the newly inserted item, you must movePrevious first.
moveEnd
public void moveEnd()
- Move the cursor to just past the end. Thus, to access the last element,
you must movePrevious.
movePrevious
public void movePrevious()
- Moves cursor back 1, or throws exception if there is none.
moveNext
public void moveNext()
- Moves cursor forward 1, or throws exception if there is none.
hasNext
public boolean hasNext()
- Returns whether moveNext() would succeed right now.
hasPrevious
public boolean hasPrevious()
- Returns whether movePrevious() would succeed right now.
getCurrent
public String getCurrent()
- Returns item in history at current position, or throws exception if none.
size
public int size()
- Returns the number of items in this History.
clear
public void clear()
- Clears the vector
getHistoryAsString
public String getHistoryAsString()
- Returns the history as a string by concatenating each string in the vector
separated by the delimiting character
writeToFile
public void writeToFile(FileSaveSelector selector)
throws IOException
- Writes this History to a the file selected in the FileSaveSelector