+
+ 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;