*/
private String filename = "";
+ /**
+ * If true, hide the mouse after typing a keystroke.
+ */
+ private boolean hideMouseWhenTyping = true;
+
+ /**
+ * If true, the mouse should not be displayed because a keystroke was
+ * typed.
+ */
+ private boolean typingHidMouse = false;
+
// ------------------------------------------------------------------------
// Constructors -----------------------------------------------------------
// ------------------------------------------------------------------------
// Use TWidget's code to pass the event to the children.
super.onMouseDown(mouse);
+ if (hideMouseWhenTyping) {
+ typingHidMouse = false;
+ }
+
if (mouseOnEditor(mouse)) {
// The editor might have changed, update the scollbars.
setBottomValue(editField.getMaximumRowNumber());
// Use TWidget's code to pass the event to the children.
super.onMouseUp(mouse);
+ if (hideMouseWhenTyping) {
+ typingHidMouse = false;
+ }
+
if (mouse.isMouse1() && mouseOnVerticalScroller(mouse)) {
// Clicked on vertical scrollbar
editField.setVisibleRowNumber(getVerticalValue());
// Use TWidget's code to pass the event to the children.
super.onMouseMotion(mouse);
+ if (hideMouseWhenTyping) {
+ typingHidMouse = false;
+ }
+
if (mouseOnEditor(mouse) && mouse.isMouse1()) {
// The editor might have changed, update the scollbars.
setBottomValue(editField.getMaximumRowNumber());
*/
@Override
public void onKeypress(final TKeypressEvent keypress) {
+ if (hideMouseWhenTyping) {
+ typingHidMouse = true;
+ }
+
// Use TWidget's code to pass the event to the children.
super.onKeypress(keypress);
super.onCommand(command);
}
+ /**
+ * Returns true if this window does not want the application-wide mouse
+ * cursor drawn over it.
+ *
+ * @return true if this window does not want the application-wide mouse
+ * cursor drawn over it
+ */
+ @Override
+ public boolean hasHiddenMouse() {
+ return (super.hasHiddenMouse() || typingHidMouse);
+ }
+
// ------------------------------------------------------------------------
// TEditorWindow ----------------------------------------------------------
// ------------------------------------------------------------------------
i18n.getString("statusBarOpen"));
statusBar.addShortcutKeypress(kbF10, cmMenu,
i18n.getString("statusBarMenu"));
+
+ // Hide mouse when typing option
+ if (System.getProperty("jexer.TEditor.hideMouseWhenTyping",
+ "true").equals("false")) {
+
+ hideMouseWhenTyping = false;
+ }
}
/**
return lines.get(lineNumber).getCursor();
}
+ /**
+ * Get the character at the current cursor position in the text.
+ *
+ * @return the character, or -1 if the cursor is at the end of the line
+ */
+ public int getChar() {
+ return lines.get(lineNumber).getChar();
+ }
+
/**
* Set the current cursor position of the editing line. 0-based.
*
}
/**
- * Decrement the cursor by one. If at the first column, do nothing.
+ * Decrement the cursor by one. If at the first column on the first
+ * line, do nothing.
*
* @return true if the cursor position changed
*/
}
/**
- * Increment the cursor by one. If at the last column, do nothing.
+ * Increment the cursor by one. If at the last column on the last line,
+ * do nothing.
*
* @return true if the cursor position changed
*/
return true;
}
+ /**
+ * Go back to the beginning of this word if in the middle, or the
+ * beginning of the previous word.
+ */
+ public void backwardsWord() {
+
+ // If at the beginning of a word already, push past it.
+ if ((getChar() != -1)
+ && (getRawLine().length() > 0)
+ && !Character.isSpace((char) getChar())
+ ) {
+ left();
+ }
+
+ // int line = lineNumber;
+ while ((getChar() == -1)
+ || (getRawLine().length() == 0)
+ || Character.isSpace((char) getChar())
+ ) {
+ if (left() == false) {
+ return;
+ }
+ }
+
+
+ assert (getChar() != -1);
+
+ if (!Character.isSpace((char) getChar())
+ && (getRawLine().length() > 0)
+ ) {
+ // Advance until at the beginning of the document or a whitespace
+ // is encountered.
+ while (!Character.isSpace((char) getChar())) {
+ int line = lineNumber;
+ if (left() == false) {
+ // End of document, bail out.
+ return;
+ }
+ if (lineNumber != line) {
+ // We wrapped a line. Here that counts as whitespace.
+ right();
+ return;
+ }
+ }
+ }
+
+ // We went one past the word, push back to the first character of
+ // that word.
+ right();
+ return;
+ }
+
+ /**
+ * Go to the beginning of the next word.
+ */
+ public void forwardsWord() {
+ int line = lineNumber;
+ while ((getChar() == -1)
+ || (getRawLine().length() == 0)
+ ) {
+ if (right() == false) {
+ return;
+ }
+ if (lineNumber != line) {
+ // We wrapped a line. Here that counts as whitespace.
+ if (!Character.isSpace((char) getChar())) {
+ // We found a character immediately after the line.
+ // Done!
+ return;
+ }
+ // Still looking...
+ line = lineNumber;
+ }
+ }
+ assert (getChar() != -1);
+
+ if (!Character.isSpace((char) getChar())
+ && (getRawLine().length() > 0)
+ ) {
+ // Advance until at the end of the document or a whitespace is
+ // encountered.
+ while (!Character.isSpace((char) getChar())) {
+ line = lineNumber;
+ if (right() == false) {
+ // End of document, bail out.
+ return;
+ }
+ if (lineNumber != line) {
+ // We wrapped a line. Here that counts as whitespace.
+ if (!Character.isSpace((char) getChar())
+ && (getRawLine().length() > 0)
+ ) {
+ // We found a character immediately after the line.
+ // Done!
+ return;
+ }
+ break;
+ }
+ }
+ }
+
+ while ((getChar() == -1)
+ || (getRawLine().length() == 0)
+ ) {
+ if (right() == false) {
+ return;
+ }
+ if (lineNumber != line) {
+ // We wrapped a line. Here that counts as whitespace.
+ if (!Character.isSpace((char) getChar())) {
+ // We found a character immediately after the line.
+ // Done!
+ return;
+ }
+ // Still looking...
+ line = lineNumber;
+ }
+ }
+ assert (getChar() != -1);
+
+ if (Character.isSpace((char) getChar())) {
+ // Advance until at the end of the document or a non-whitespace
+ // is encountered.
+ while (Character.isSpace((char) getChar())) {
+ if (right() == false) {
+ // End of document, bail out.
+ return;
+ }
+ }
+ return;
+ }
+
+ // We wrapped the line to get here.
+ return;
+ }
+
+ /**
+ * Get the raw string that matches this line.
+ *
+ * @return the string
+ */
+ public String getRawLine() {
+ return lines.get(lineNumber).getRawString();
+ }
+
/**
* Go to the first column of this line.
*