+ /**
+ * Delete text within the selection bounds.
+ */
+ private void deleteSelection() {
+ if (!inSelection) {
+ return;
+ }
+
+ saveUndo();
+
+ inSelection = false;
+
+ int startCol = selectionColumn0;
+ int startRow = selectionLine0;
+ int endCol = selectionColumn1;
+ int endRow = selectionLine1;
+
+ /*
+ System.err.println("INITIAL: " + startRow + " " + startCol + " " +
+ endRow + " " + endCol + " " +
+ document.getLineNumber() + " " + document.getCursor());
+ */
+
+ if (((selectionColumn1 < selectionColumn0)
+ && (selectionLine1 == selectionLine0))
+ || (selectionLine1 < selectionLine0)
+ ) {
+ // The user selected from bottom-to-top and/or right-to-left.
+ // Reverse the coordinates for the inverted section.
+ startCol = selectionColumn1;
+ startRow = selectionLine1;
+ endCol = selectionColumn0;
+ endRow = selectionLine0;
+
+ if (endRow >= document.getLineCount()) {
+ // The selection started beyond EOF, trim it to EOF.
+ endRow = document.getLineCount() - 1;
+ endCol = document.getLine(endRow).getDisplayLength();
+ } else if (endRow == document.getLineCount() - 1) {
+ // The selection started beyond EOF, trim it to EOF.
+ if (endCol >= document.getLine(endRow).getDisplayLength()) {
+ endCol = document.getLine(endRow).getDisplayLength() - 1;
+ }
+ }
+ }
+ /*
+ System.err.println("FLIP: " + startRow + " " + startCol + " " +
+ endRow + " " + endCol + " " +
+ document.getLineNumber() + " " + document.getCursor());
+ System.err.println(" --END: " + endRow + " " + document.getLineCount() +
+ " " + document.getLine(endRow).getDisplayLength());
+ */
+
+ assert (endRow < document.getLineCount());
+ if (endCol >= document.getLine(endRow).getDisplayLength()) {
+ endCol = document.getLine(endRow).getDisplayLength() - 1;
+ }
+ if (endCol < 0) {
+ endCol = 0;
+ }
+ if (startCol >= document.getLine(startRow).getDisplayLength()) {
+ startCol = document.getLine(startRow).getDisplayLength() - 1;
+ }
+ if (startCol < 0) {
+ startCol = 0;
+ }
+
+ // Place the cursor on the selection end, and "press backspace" until
+ // the cursor matches the selection start.
+ /*
+ System.err.println("BEFORE: " + startRow + " " + startCol + " " +
+ endRow + " " + endCol + " " +
+ document.getLineNumber() + " " + document.getCursor());
+ */
+ document.setLineNumber(endRow);
+ document.setCursor(endCol + 1);
+ while (!((document.getLineNumber() == startRow)
+ && (document.getCursor() == startCol))
+ ) {
+ /*
+ System.err.println("DURING: " + startRow + " " + startCol + " " +
+ endRow + " " + endCol + " " +
+ document.getLineNumber() + " " + document.getCursor());
+ */
+
+ document.backspace();
+ }
+ alignTopLine(true);
+ }
+
+ /**
+ * Copy text within the selection bounds to clipboard.
+ */
+ private void copySelection() {
+ if (!inSelection) {
+ return;
+ }
+ getClipboard().copyText(getSelection());
+ }
+
+ /**
+ * Set the selection.
+ *
+ * @param startRow the starting row number. 0-based: row 0 is the first
+ * row.
+ * @param startColumn the starting column number. 0-based: column 0 is
+ * the first column.
+ * @param endRow the ending row number. 0-based: row 0 is the first row.
+ * @param endColumn the ending column number. 0-based: column 0 is the
+ * first column.
+ */
+ public void setSelection(final int startRow, final int startColumn,
+ final int endRow, final int endColumn) {
+
+ inSelection = true;
+ selectionLine0 = startRow;
+ selectionColumn0 = startColumn;
+ selectionLine1 = endRow;
+ selectionColumn1 = endColumn;
+ }
+
+ /**
+ * Copy text within the selection bounds to a string.
+ *
+ * @return the selection as a string, or null if there is no selection
+ */
+ public String getSelection() {
+ if (!inSelection) {
+ return null;
+ }
+
+ int startCol = selectionColumn0;
+ int startRow = selectionLine0;
+ int endCol = selectionColumn1;
+ int endRow = selectionLine1;
+
+ if (((selectionColumn1 < selectionColumn0)
+ && (selectionLine1 == selectionLine0))
+ || (selectionLine1 < selectionLine0)
+ ) {
+ // The user selected from bottom-to-top and/or right-to-left.
+ // Reverse the coordinates for the inverted section.
+ startCol = selectionColumn1;
+ startRow = selectionLine1;
+ endCol = selectionColumn0;
+ endRow = selectionLine0;
+ }
+
+ StringBuilder sb = new StringBuilder();
+
+ if (endRow > startRow) {
+ // First line
+ String line = document.getLine(startRow).getRawString();
+ int x = 0;
+ for (int i = 0; i < line.length(); ) {
+ int ch = line.codePointAt(i);
+
+ if (x >= startCol) {
+ sb.append(Character.toChars(ch));
+ }
+ x += StringUtils.width(ch);
+ i += Character.charCount(ch);
+ }
+ sb.append("\n");
+
+ // Middle lines
+ for (int y = startRow + 1; y < endRow; y++) {
+ sb.append(document.getLine(y).getRawString());
+ sb.append("\n");
+ }
+
+ // Final line
+ line = document.getLine(endRow).getRawString();
+ x = 0;
+ for (int i = 0; i < line.length(); ) {
+ int ch = line.codePointAt(i);
+
+ if (x > endCol) {
+ break;
+ }
+
+ sb.append(Character.toChars(ch));
+ x += StringUtils.width(ch);
+ i += Character.charCount(ch);
+ }
+ } else {
+ assert (startRow == endRow);
+
+ // Only one line
+ String line = document.getLine(startRow).getRawString();
+ int x = 0;
+ for (int i = 0; i < line.length(); ) {
+ int ch = line.codePointAt(i);
+
+ if ((x >= startCol) && (x <= endCol)) {
+ sb.append(Character.toChars(ch));
+ }
+
+ x += StringUtils.width(ch);
+ i += Character.charCount(ch);
+ }
+ }
+ return sb.toString();
+ }
+
+ /**
+ * Get the selection starting row number.
+ *
+ * @return the starting row number, or -1 if there is no selection.
+ * 0-based: row 0 is the first row.
+ */
+ public int getSelectionStartRow() {
+ if (!inSelection) {
+ return -1;
+ }
+
+ int startCol = selectionColumn0;
+ int startRow = selectionLine0;
+ int endCol = selectionColumn1;
+ int endRow = selectionLine1;
+
+ if (((selectionColumn1 < selectionColumn0)
+ && (selectionLine1 == selectionLine0))
+ || (selectionLine1 < selectionLine0)
+ ) {
+ // The user selected from bottom-to-top and/or right-to-left.
+ // Reverse the coordinates for the inverted section.
+ startCol = selectionColumn1;
+ startRow = selectionLine1;
+ endCol = selectionColumn0;
+ endRow = selectionLine0;
+ }
+ return startRow;
+ }
+
+ /**
+ * Get the selection starting column number.
+ *
+ * @return the starting column number, or -1 if there is no selection.
+ * 0-based: column 0 is the first column.
+ */
+ public int getSelectionStartColumn() {
+ if (!inSelection) {
+ return -1;
+ }
+
+ int startCol = selectionColumn0;
+ int startRow = selectionLine0;
+ int endCol = selectionColumn1;
+ int endRow = selectionLine1;
+
+ if (((selectionColumn1 < selectionColumn0)
+ && (selectionLine1 == selectionLine0))
+ || (selectionLine1 < selectionLine0)
+ ) {
+ // The user selected from bottom-to-top and/or right-to-left.
+ // Reverse the coordinates for the inverted section.
+ startCol = selectionColumn1;
+ startRow = selectionLine1;
+ endCol = selectionColumn0;
+ endRow = selectionLine0;
+ }
+ return startCol;
+ }
+
+ /**
+ * Get the selection ending row number.
+ *
+ * @return the ending row number, or -1 if there is no selection.
+ * 0-based: row 0 is the first row.
+ */
+ public int getSelectionEndRow() {
+ if (!inSelection) {
+ return -1;
+ }
+
+ int startCol = selectionColumn0;
+ int startRow = selectionLine0;
+ int endCol = selectionColumn1;
+ int endRow = selectionLine1;
+
+ if (((selectionColumn1 < selectionColumn0)
+ && (selectionLine1 == selectionLine0))
+ || (selectionLine1 < selectionLine0)
+ ) {
+ // The user selected from bottom-to-top and/or right-to-left.
+ // Reverse the coordinates for the inverted section.
+ startCol = selectionColumn1;
+ startRow = selectionLine1;
+ endCol = selectionColumn0;
+ endRow = selectionLine0;
+ }
+ return endRow;
+ }
+
+ /**
+ * Get the selection ending column number.
+ *
+ * @return the ending column number, or -1 if there is no selection.
+ * 0-based: column 0 is the first column.
+ */
+ public int getSelectionEndColumn() {
+ if (!inSelection) {
+ return -1;
+ }
+
+ int startCol = selectionColumn0;
+ int startRow = selectionLine0;
+ int endCol = selectionColumn1;
+ int endRow = selectionLine1;
+
+ if (((selectionColumn1 < selectionColumn0)
+ && (selectionLine1 == selectionLine0))
+ || (selectionLine1 < selectionLine0)
+ ) {
+ // The user selected from bottom-to-top and/or right-to-left.
+ // Reverse the coordinates for the inverted section.
+ startCol = selectionColumn1;
+ startRow = selectionLine1;
+ endCol = selectionColumn0;
+ endRow = selectionLine0;
+ }
+ return endCol;
+ }
+
+ /**
+ * Unset the selection.
+ */
+ public void unsetSelection() {
+ inSelection = false;
+ }
+
+ /**
+ * Replace whatever is being selected with new text. If not in
+ * selection, nothing is replaced.
+ *
+ * @param text the new replacement text
+ */
+ public void replaceSelection(final String text) {
+ if (!inSelection) {
+ return;
+ }
+
+ // Delete selected text, then paste text from clipboard.
+ deleteSelection();
+
+ for (int i = 0; i < text.length(); ) {
+ int ch = text.codePointAt(i);
+ switch (ch) {
+ case '\n':
+ onKeypress(new TKeypressEvent(kbEnter));
+ break;
+ case '\t':
+ onKeypress(new TKeypressEvent(kbTab));
+ break;
+ default:
+ if ((ch >= 0x20) && (ch != 0x7F)) {
+ onKeypress(new TKeypressEvent(false, 0, ch,
+ false, false, false));
+ }
+ break;
+ }
+ i += Character.charCount(ch);
+ }
+ }
+
+ /**
+ * Check if selection is available.
+ *
+ * @return true if a selection has been made
+ */
+ public boolean hasSelection() {
+ return inSelection;
+ }
+
+ /**
+ * Get the entire contents of the editor as one string.
+ *
+ * @return the editor contents
+ */
+ public String getText() {
+ return document.getText();
+ }
+
+ /**
+ * Set the entire contents of the editor from one string.
+ *
+ * @param text the new contents
+ */
+ public void setText(final String text) {
+ document = new Document(text, defaultColor);
+ unsetSelection();
+ topLine = 0;
+ leftColumn = 0;
+ }
+
+ // ------------------------------------------------------------------------
+ // EditMenuUser -----------------------------------------------------------
+ // ------------------------------------------------------------------------
+
+ /**
+ * Check if the cut menu item should be enabled.
+ *
+ * @return true if the cut menu item should be enabled
+ */
+ public boolean isEditMenuCut() {
+ return true;
+ }
+
+ /**
+ * Check if the copy menu item should be enabled.
+ *
+ * @return true if the copy menu item should be enabled
+ */
+ public boolean isEditMenuCopy() {
+ return true;
+ }
+
+ /**
+ * Check if the paste menu item should be enabled.
+ *
+ * @return true if the paste menu item should be enabled
+ */
+ public boolean isEditMenuPaste() {
+ return true;
+ }
+
+ /**
+ * Check if the clear menu item should be enabled.
+ *
+ * @return true if the clear menu item should be enabled
+ */
+ public boolean isEditMenuClear() {
+ return true;
+ }
+
+ /**
+ * Save undo state.
+ */
+ private void saveUndo() {
+ SavedState state = new SavedState();
+ state.document = document.dup();
+ state.topLine = topLine;
+ state.leftColumn = leftColumn;
+ if (undoLevel > 0) {
+ while (undoList.size() > undoLevel) {
+ undoList.remove(0);
+ }
+ }
+ undoList.add(state);
+ undoListI = undoList.size() - 1;
+ }
+
+ /**
+ * Undo an edit.
+ */
+ public void undo() {
+ inSelection = false;
+ if ((undoListI >= 0) && (undoListI < undoList.size())) {
+ SavedState state = undoList.get(undoListI);
+ document = state.document.dup();
+ topLine = state.topLine;
+ leftColumn = state.leftColumn;
+ undoListI--;
+ setCursorY(document.getLineNumber() - topLine);
+ alignCursor();
+ }
+ }
+
+ /**
+ * Redo an edit.
+ */
+ public void redo() {
+ inSelection = false;
+ if ((undoListI >= 0) && (undoListI < undoList.size())) {
+ SavedState state = undoList.get(undoListI);
+ document = state.document.dup();
+ topLine = state.topLine;
+ leftColumn = state.leftColumn;
+ undoListI++;
+ setCursorY(document.getLineNumber() - topLine);
+ alignCursor();
+ }
+ }
+
+ /**
+ * Trim trailing whitespace from lines and trailing empty
+ * lines from the document.
+ */
+ public void cleanWhitespace() {
+ document.cleanWhitespace();
+ setCursorY(document.getLineNumber() - topLine);
+ alignCursor();
+ }
+
+ /**
+ * Set keyword highlighting.
+ *
+ * @param enabled if true, enable keyword highlighting
+ */
+ public void setHighlighting(final boolean enabled) {
+ document.setHighlighting(enabled);
+ }
+