JEditTextArea.java

Go to the documentation of this file.

/*
 * JEditTextArea.java - jEdit's text component
 * Copyright (C) 1999 Slava Pestov
 * Copyright (C) 2000-2023 The Gridarta Developers.
 *
 * You may use and modify this package for any purpose. Redistribution is
 * permitted, in both source and binary form, provided that this notice
 * remains intact in all source distributions of this package.
 */
 
package net.sf.gridarta.textedit.textarea;
 
import java.awt.AWTEvent;
import java.awt.Adjustable;
import java.awt.Font;
import java.awt.datatransfer.Clipboard;
import java.awt.datatransfer.DataFlavor;
import java.awt.datatransfer.StringSelection;
import java.awt.datatransfer.UnsupportedFlavorException;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.AdjustmentEvent;
import java.awt.event.AdjustmentListener;
import java.awt.event.ComponentAdapter;
import java.awt.event.ComponentEvent;
import java.awt.event.FocusEvent;
import java.awt.event.FocusListener;
import java.awt.event.InputEvent;
import java.awt.event.KeyEvent;
import java.awt.event.MouseAdapter;
import java.awt.event.MouseEvent;
import java.awt.event.MouseMotionListener;
import java.awt.event.MouseWheelEvent;
import java.io.IOException;
import java.lang.reflect.Field;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.HashSet;
import java.util.Set;
import javax.swing.JComponent;
import javax.swing.JPopupMenu;
import javax.swing.JScrollBar;
import javax.swing.KeyStroke;
import javax.swing.SwingUtilities;
import javax.swing.Timer;
import javax.swing.event.DocumentEvent;
import javax.swing.event.DocumentEvent.ElementChange;
import javax.swing.event.DocumentListener;
import javax.swing.text.BadLocationException;
import javax.swing.text.Document;
import javax.swing.text.Segment;
import javax.swing.undo.AbstractUndoableEdit;
import javax.swing.undo.CannotRedoException;
import javax.swing.undo.CannotUndoException;
import javax.swing.undo.UndoableEdit;
import org.apache.log4j.Category;
import org.apache.log4j.Logger;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
 
public class JEditTextArea extends JComponent {
 
    private static final Category LOG = Logger.getLogger(JEditTextArea.class);
 
    private static final long serialVersionUID = 1L;
 
    @NotNull
    private String unmodifiedText = "";
 
    @Nullable
    private static JEditTextArea focusedComponent;
 
    @NotNull
    private static final Timer CARET_TIMER = new Timer(500, new CaretBlinker());
 
    static {
        CARET_TIMER.setInitialDelay(500);
        CARET_TIMER.start();
    }
 
    @NotNull
    private final TextAreaPainter painter;
 
    @Nullable
    private final JPopupMenu popup;
 
    @NotNull
    private final TextAreaCaret caret;
 
    @NotNull
    private final JScrollBar vertical = new JScrollBar(Adjustable.VERTICAL);
 
    @NotNull
    private final JScrollBar horizontal = new JScrollBar(Adjustable.HORIZONTAL);
 
    private boolean scrollBarsInitialized;
 
    @NotNull
    private final InputHandler inputHandler;
 
    @NotNull
    private final SyntaxDocument document;
 
    @NotNull
    private final TextAreaSelection selection;
 
    @NotNull
    private final TextAreaBrackets brackets = new TextAreaBrackets();
 
    @NotNull
    private final TextAreaConfig config;
 
    public JEditTextArea(@NotNull final TextAreaDefaults defaults, @NotNull final SyntaxDocument document, final boolean paintInvalid) {
        // Enable the necessary events
        enableEvents(AWTEvent.KEY_EVENT_MASK);
 
        // Initialize some misc. stuff
        caret = new TextAreaCaret(defaults.getCaretVisible(), defaults.getCaretBlinks());
        selection = new TextAreaSelection(document);
        config = new TextAreaConfig(defaults.getEditable(), defaults.getElectricScroll());
        painter = new TextAreaPainter(this, selection, caret, defaults, brackets, config, paintInvalid);
        painter.recalculateVisibleLines();
 
        // Initialize the GUI
        setLayout(new ScrollLayout(this));
        add(ScrollLayout.CENTER, painter);
        add(ScrollLayout.RIGHT, vertical);
        add(ScrollLayout.BOTTOM, horizontal);
 
        // Add some event listeners
        vertical.addAdjustmentListener(new AdjustHandler());
        horizontal.addAdjustmentListener(new AdjustHandler());
        painter.addComponentListener(new ComponentHandler());
        final MouseHandler mouseHandler = new MouseHandler();
        painter.addMouseListener(mouseHandler);
        painter.addMouseWheelListener(mouseHandler);
        painter.addMouseMotionListener(new DragHandler());
        addFocusListener(new FocusHandler());
 
        // Load the defaults
        inputHandler = defaults.getInputHandler();
        this.document = document;
        document.addDocumentListener(new DocumentHandler());
        select(0, 0);
        updateScrollBars();
 
        popup = defaults.getPopup();
 
        // free tab key from the focus traversal manager
        freeTabKeyFromFocusTraversal();
 
        // We don't seem to get the initial focus event?
        focusedComponent = this;
    }
 
    private void freeTabKeyFromFocusTraversal() {
        try {
            // preparing the key set first, this should be harmless
            final Set<KeyStroke> forwardTraversalKeys = new HashSet<>();
            forwardTraversalKeys.add(KeyStroke.getKeyStroke("control TAB"));
 
            // here we try to access java.awt.KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS
            final Field field = Class.forName("java.awt.KeyboardFocusManager").getField("FORWARD_TRAVERSAL_KEYS");
            final Integer value = field.getInt(field); // store the value of this field
 
            for (final Method method : getClass().getMethods()) {
                // here we try to find the method "setFocusTraversalKeys", and execute it if found
                if (method.getName().equalsIgnoreCase("setFocusTraversalKeys")) {
                    method.invoke(this, value, forwardTraversalKeys);
                    // System.err.println("freeTabKeyFromFocusTraversal() succeeded!");
                }
            }
        } catch (final ClassNotFoundException | IllegalAccessException | InvocationTargetException | NoSuchFieldException ignored) {
            // ignore
        }
    }
 
    @Override
    public void setFont(@NotNull final Font font) {
        painter.setFont(font);
    }
 
    @NotNull
    public InputHandler getInputHandler() {
        return inputHandler;
    }
 
    private void setCaretVisible(final boolean caretVisible) {
        caret.setCaretVisible(caretVisible);
        painter.invalidateSelectedLines();
    }
 
    private void blinkCaret() {
        if (caret.blinkCaret()) {
            painter.invalidateSelectedLines();
        }
    }
 
    public int getElectricScroll() {
        return config.getElectricScroll();
    }
 
    public void updateScrollBars() {
        final int visibleLines = getVisibleLines();
        if (visibleLines != 0) {
            vertical.setValues(painter.getFirstLine(), visibleLines, 0, selection.getLineCount());
            //vertical.setUnitIncrement(2);
            vertical.setUnitIncrement(1); // scroll one line per click
            vertical.setBlockIncrement(visibleLines);
        }
 
        final int width = painter.getWidth();
        if (width != 0) {
            horizontal.setValues(-painter.getHorizontalOffset(), width, 0, width * 5);
            //horizontal.setUnitIncrement(painter.getFontMetrics().charWidth('w'));
            horizontal.setUnitIncrement(painter.getDefaultCharWidth());
            horizontal.setBlockIncrement(width / 2);
        }
    }
 
    public int getFirstLine() {
        return painter.getFirstLine();
    }
 
    public void setFirstLine(final int firstLine) {
        if (!painter.setFirstLine(firstLine)) {
            return;
        }
 
        if (firstLine != vertical.getValue()) {
            updateScrollBars();
        }
        painter.repaint();
    }
 
    public int getVisibleLines() {
        return painter.getVisibleLines();
    }
 
    private void setHorizontalOffset(final int horizontalOffset) {
        if (!painter.setHorizontalOffset(horizontalOffset)) {
            return;
        }
 
        if (horizontalOffset != horizontal.getValue()) {
            updateScrollBars();
        }
 
        painter.repaint();
    }
 
    private void setOrigin(final int firstLine, final int horizontalOffset) {
        boolean changed = false;
 
        if (painter.setHorizontalOffset(horizontalOffset)) {
            changed = true;
        }
 
        if (painter.setFirstLine(firstLine)) {
            changed = true;
        }
 
        if (changed) {
            updateScrollBars();
            painter.repaint();
        }
    }
 
    private void scrollToCaret() {
        final int line = selection.getCaretLine();
        final int lineStart = selection.getLineStartOffset(line);
        final int offset = Math.max(0, Math.min(selection.getLineLength(line) - 1, selection.getCaretPosition() - lineStart));
 
        scrollTo(line, offset);
    }
 
    public void setEditingFocus() {
        try {
            requestFocus();
            setCaretVisible(true);
            focusedComponent = this;
            setCaretPosition(0); // set caret to 0, 0 coordinates
        } catch (final NullPointerException e) {
            LOG.error("Null Pointer Exception in JEditTextArea.setEditingFocus()");
        }
    }
 
    private void scrollTo(final int line, final int offset) {
        // visibleLines == 0 before the component is realized
        // we can't do any proper scrolling then, so we have
        // this hack...
        final int visibleLines = getVisibleLines();
        final int electricScroll = config.getElectricScroll();
        if (visibleLines == 0) {
            setFirstLine(Math.max(0, line - electricScroll));
            return;
        }
 
        int newFirstLine = painter.getFirstLine();
        final int horizontalOffset = painter.getHorizontalOffset();
 
        if (line < newFirstLine + electricScroll) {
            newFirstLine = Math.max(0, line - electricScroll);
        } else if (line + electricScroll >= newFirstLine + visibleLines) {
            newFirstLine = (line - visibleLines) + electricScroll + 1;
            if (newFirstLine + visibleLines >= selection.getLineCount()) {
                newFirstLine = selection.getLineCount() - visibleLines;
            }
            if (newFirstLine < 0) {
                newFirstLine = 0;
            }
        }
 
        final int x = painter.offsetToX2(line, offset);
        final int width = painter.getFontMetrics().charWidth('w');
 
        int newHorizontalOffset = horizontalOffset;
        if (x < 0) {
            newHorizontalOffset = Math.min(0, horizontalOffset - x + width + 5);
        } else if (x + width >= painter.getWidth()) {
            newHorizontalOffset = horizontalOffset + (painter.getWidth() - x) - width - 5;
        }
 
        setOrigin(newFirstLine, newHorizontalOffset);
    }
 
    public int lineToY(final int line) {
        return painter.lineToY(line);
    }
 
    public int offsetToX(final int line, final int offset) {
        return painter.offsetToX(line, offset);
    }
 
    public int offsetToX2(final int line, final int offset) {
        return painter.offsetToX2(line, offset);
    }
 
    public int xToOffset(final int line, final int x) {
        return painter.xToOffset(line, x);
    }
 
    @NotNull
    public Document getDocument() {
        return selection.getDocument();
    }
 
    public int getDocumentLength() {
        return selection.getDocumentLength();
    }
 
    public int getLineCount() {
        return selection.getLineCount();
    }
 
    public int getLineStartOffset(final int line) {
        return selection.getLineStartOffset(line);
    }
 
    public int getLineEndOffset(final int line) {
        return selection.getLineEndOffset(line);
    }
 
    @NotNull
    public String getText() {
        return selection.getText();
    }
 
    public void setText(@NotNull final String text) {
        selection.setText(text);
    }
 
    @Nullable
    public String getText(final int start, final int len) {
        return selection.getText(start, len);
    }
 
    public void getText(final int start, final int len, @NotNull final Segment segment) {
        selection.getText(start, len, segment);
    }
 
    @NotNull
    public CharSequence getLineText(final int lineIndex) {
        return selection.getLineText(lineIndex);
    }
 
    public int getSelectionStart() {
        return selection.getSelectionStart();
    }
 
    public int getSelectionEnd() {
        return selection.getSelectionEnd();
    }
 
    public int getCaretPosition() {
        return selection.getCaretPosition();
    }
 
    public int getCaretLine() {
        return selection.getCaretLine();
    }
 
    public int getMarkPosition() {
        return selection.getMarkPosition();
    }
 
    public void setCaretPosition(final int caret) {
        select(caret, caret);
    }
 
    public void selectAll() {
        select(0, getDocumentLength());
    }
 
    public void select(final int start, final int end) {
        final int newStart;
        final int newEnd;
        final boolean newBias;
        if (start <= end) {
            newStart = start;
            newEnd = end;
            newBias = false;
        } else {
            newStart = end;
            newEnd = start;
            newBias = true;
        }
 
        if (newStart < 0 || newEnd > getDocumentLength()) {
            throw new IllegalArgumentException("Bounds out of range: " + newStart + ", " + newEnd);
        }
 
        // If the new position is the same as the old, we don't
        // do all this crap, however we still do the stuff at
        // the end (clearing magic position, scrolling)
        if (newStart != selection.getSelectionStart() || newEnd != selection.getSelectionEnd() || newBias != selection.getBiasLeft()) {
            final int newStartLine = selection.getLineOfOffset(newStart);
            final int newEndLine = selection.getLineOfOffset(newEnd);
 
            if (painter.isBracketHighlightEnabled()) {
                final int oldBracketLine = brackets.getBracketLine();
                if (oldBracketLine != -1) {
                    painter.invalidateLine(oldBracketLine);
                }
                updateBracketHighlight(end);
                final int newBracketLine = brackets.getBracketLine();
                if (newBracketLine != -1) {
                    painter.invalidateLine(newBracketLine);
                }
            }
 
            painter.invalidateLineRange(selection.getSelectionStartLine(), selection.getSelectionEndLine());
            painter.invalidateLineRange(newStartLine, newEndLine);
 
            SyntaxDocument.addUndoableEdit(new CaretUndo(selection.getSelectionStart(), selection.getSelectionEnd()));
            selection.setSelection(newStart, newEnd, newStartLine, newEndLine, newBias);
        }
 
        // When the user is typing, etc, we don't want the caret
        // to blink
        caret.setBlink(true);
        CARET_TIMER.restart();
 
        selection.disableSelectionIfEmpty();
 
        config.setMagicCaret(-1); // Clear the `magic' caret position used by up/down
 
        scrollToCaret();
    }
 
    @Nullable
    public String getSelectedText() {
        return selection.getSelectedText();
    }
 
    public void setSelectedText(@NotNull final String selectedText) {
        if (!config.isEditable()) {
            throw new InternalError("Text component read only");
        }
 
        selection.setSelectedText(selectedText);
 
        setCaretPosition(selection.getSelectionEnd());
    }
 
    public boolean isEditable() {
        return config.isEditable();
    }
 
    public int getMagicCaretPosition() {
        return config.getMagicCaret();
    }
 
    public void setMagicCaretPosition(final int magicCaret) {
        config.setMagicCaret(magicCaret);
    }
 
    public void overwriteSetSelectedText(@NotNull final String str) {
        // Don't overstrike if there is a selection
        if (!config.isOverwrite() || selection.getSelectionStart() != selection.getSelectionEnd()) {
            setSelectedText(str);
            return;
        }
 
        // Don't overstrike if we're on the end of
        // the line
        final int caret = selection.getCaretPosition();
        final int caretLineEnd = selection.getLineEndOffset(selection.getCaretLine());
        if (caretLineEnd - caret <= str.length()) {
            setSelectedText(str);
            return;
        }
 
        SyntaxDocument.beginCompoundEdit();
 
        try {
            document.remove(caret, str.length());
            document.insertString(caret, str, null);
        } catch (final BadLocationException bl) {
            bl.printStackTrace();
        } finally {
            SyntaxDocument.endCompoundEdit();
        }
    }
 
    public boolean isOverwriteEnabled() {
        return config.isOverwrite();
    }
 
    public void setOverwriteEnabled(final boolean overwrite) {
        config.setOverwrite(overwrite);
        painter.invalidateSelectedLines();
    }
 
    public boolean isSelectionRectangular() {
        return selection.isSelectionRectangular();
    }
 
    public void setSelectionRectangular(final boolean rectangleSelect) {
        selection.setSelectionRectangular(rectangleSelect);
        painter.invalidateSelectedLines();
    }
 
    public void cut() {
        if (config.isEditable()) {
            copy();
            setSelectedText("");
        }
    }
 
    private void copy() {
        if (selection.getSelectionStart() != selection.getSelectionEnd()) {
            final Clipboard clipboard = getToolkit().getSystemClipboard();
 
            final String selection = this.selection.getSelectedText();
 
            final int repeatCount = inputHandler.getRepeatCount();
            final StringBuilder buf = new StringBuilder();
            for (int i = 0; i < repeatCount; i++) {
                buf.append(selection);
            }
 
            clipboard.setContents(new StringSelection(buf.toString()), null);
        }
    }
 
    public void paste() {
        if (config.isEditable()) {
            final Clipboard clipboard = getToolkit().getSystemClipboard();
            try {
                // The MacOS MRJ doesn't convert \r to \n,
                // so do it here
                final String selection = ((String) clipboard.getContents(this).getTransferData(DataFlavor.stringFlavor)).replace('\r', '\n');
 
                final int repeatCount = inputHandler.getRepeatCount();
                final StringBuilder buf = new StringBuilder();
                for (int i = 0; i < repeatCount; i++) {
                    buf.append(selection);
                }
                setSelectedText(buf.toString());
            } catch (final IOException | UnsupportedFlavorException e) {
                getToolkit().beep();
                LOG.error("Clipboard does not contain a string");
            }
        }
    }
 
    @Override
    public void removeNotify() {
        super.removeNotify();
        if (focusedComponent == this) {
            focusedComponent = null;
        }
    }
 
    @Override
    public void processKeyEvent(@NotNull final KeyEvent e) {
        switch (e.getID()) {
        case KeyEvent.KEY_TYPED:
            inputHandler.keyTyped(e);
            break;
 
        case KeyEvent.KEY_PRESSED:
            inputHandler.keyPressed(e);
            break;
 
        case KeyEvent.KEY_RELEASED:
            inputHandler.keyReleased(e);
            break;
        }
 
        super.processKeyEvent(e);
    }
 
    private void updateBracketHighlight(final int newCaretPosition) {
        if (newCaretPosition == 0) {
            brackets.clear();
            return;
        }
 
        try {
            final int offset = TextUtilities.findMatchingBracket(document, newCaretPosition - 1);
            if (offset != -1) {
                final int bracketLine = selection.getLineOfOffset(offset);
                final int bracketPosition = offset - selection.getLineStartOffset(bracketLine);
                brackets.set(bracketPosition, bracketLine);
                return;
            }
        } catch (final BadLocationException bl) {
            bl.printStackTrace();
        }
 
        brackets.clear();
    }
 
    private void documentChanged(@NotNull final DocumentEvent evt) {
        final ElementChange ch = evt.getChange(document.getDefaultRootElement());
        final int count = ch == null ? 0 : ch.getChildrenAdded().length - ch.getChildrenRemoved().length;
        final int line = selection.getLineOfOffset(evt.getOffset());
        if (count == 0) {
            painter.invalidateLine(line);
        } else {
            final int firstLine = painter.getFirstLine();
            if (line < firstLine) {
                // do magic stuff
                setFirstLine(firstLine + count);
                // end of magic stuff
            } else {
                painter.invalidateLineRange(line, firstLine + getVisibleLines());
                updateScrollBars();
            }
        }
    }
 
    public boolean isModified() {
        return !unmodifiedText.equals(selection.getText());
    }
 
    public void resetModified() {
        unmodifiedText = selection.getText();
    }
 
    private static class CaretBlinker implements ActionListener {
 
        @Override
        public void actionPerformed(@NotNull final ActionEvent e) {
            if (focusedComponent != null && focusedComponent.hasFocus()) {
                focusedComponent.blinkCaret();
            }
        }
 
    }
 
    private class AdjustHandler implements AdjustmentListener {
 
        @Override
        public void adjustmentValueChanged(@NotNull final AdjustmentEvent e) {
            if (!scrollBarsInitialized) {
                return;
            }
 
            // If this is not done, mousePressed events accumulate
            // and the result is that scrolling doesn't stop after
            // the mouse is released
            SwingUtilities.invokeLater(() -> {
                if (e.getAdjustable() == vertical) {
                    setFirstLine(vertical.getValue());
                } else {
                    setHorizontalOffset(-horizontal.getValue());
                }
            });
        }
 
    }
 
    private class ComponentHandler extends ComponentAdapter {
 
        @Override
        public void componentResized(@NotNull final ComponentEvent e) {
            painter.recalculateVisibleLines();
            scrollBarsInitialized = true;
        }
 
    }
 
    private class DocumentHandler implements DocumentListener {
 
        @Override
        public void insertUpdate(@NotNull final DocumentEvent e) {
            documentChanged(e);
 
            final int offset = e.getOffset();
            final int length = e.getLength();
            final int selectionStart = selection.getSelectionStart();
            final int selectionEnd = selection.getSelectionEnd();
 
            final int newStart;
            if (selectionStart > offset || (selectionStart == selectionEnd && selectionStart == offset)) {
                newStart = selectionStart + length;
            } else {
                newStart = selectionStart;
            }
 
            final int newEnd;
            if (selectionEnd >= offset) {
                newEnd = selectionEnd + length;
            } else {
                newEnd = selectionEnd;
            }
 
            select(newStart, newEnd);
        }
 
        @Override
        public void removeUpdate(@NotNull final DocumentEvent e) {
            documentChanged(e);
 
            final int offset = e.getOffset();
            final int length = e.getLength();
            final int selectionStart = selection.getSelectionStart();
            final int selectionEnd = selection.getSelectionEnd();
 
            final int newStart;
            if (selectionStart > offset) {
                if (selectionStart > offset + length) {
                    newStart = selectionStart - length;
                } else {
                    newStart = offset;
                }
            } else {
                newStart = selectionStart;
            }
 
            final int newEnd;
            if (selectionEnd > offset) {
                if (selectionEnd > offset + length) {
                    newEnd = selectionEnd - length;
                } else {
                    newEnd = offset;
                }
            } else {
                newEnd = selectionEnd;
            }
 
            select(newStart, newEnd);
        }
 
        @Override
        public void changedUpdate(@NotNull final DocumentEvent e) {
        }
 
    }
 
    private class DragHandler implements MouseMotionListener {
 
        @Override
        public void mouseDragged(@NotNull final MouseEvent e) {
            if (popup != null && popup.isVisible()) {
                return;
            }
 
            setSelectionRectangular((e.getModifiers() & InputEvent.CTRL_MASK) != 0);
            select(selection.getMarkPosition(), painter.xyToOffset(e.getX(), e.getY()));
        }
 
        @Override
        public void mouseMoved(@NotNull final MouseEvent e) {
        }
 
    }
 
    private class FocusHandler implements FocusListener {
 
        @Override
        public void focusGained(@NotNull final FocusEvent e) {
            setCaretVisible(true);
            focusedComponent = JEditTextArea.this;
        }
 
        @Override
        public void focusLost(@NotNull final FocusEvent e) {
            setCaretVisible(false);
            focusedComponent = null;
        }
 
    }
 
    private class MouseHandler extends MouseAdapter {
 
        @Override
        public void mousePressed(@NotNull final MouseEvent e) {
            requestFocus();
 
            // Focus events not fired sometimes?
            setCaretVisible(true);
            focusedComponent = JEditTextArea.this;
 
            if ((e.getModifiers() & InputEvent.BUTTON3_MASK) != 0 && popup != null) {
                popup.show(painter, e.getX(), e.getY());
                return;
            }
 
            final int line = painter.yToLine(e.getY());
            final int offset = xToOffset(line, e.getX());
            final int dot = selection.getLineStartOffset(line) + offset;
 
            switch (e.getClickCount()) {
            case 1:
                doSingleClick(e, dot);
                break;
            case 2:
                doDoubleClick(line, offset, dot);
                break;
            case 3:
                doTripleClick(line);
                break;
            }
        }
 
        @Override
        public void mouseWheelMoved(@NotNull final MouseWheelEvent e) {
            final int diff;
            if (e.getScrollType() == MouseWheelEvent.WHEEL_UNIT_SCROLL) {
                diff = e.getUnitsToScroll() * vertical.getUnitIncrement(1);
            } else {
                diff = e.getWheelRotation() * vertical.getBlockIncrement();
            }
            vertical.setValue(vertical.getValue() + diff);
        }
 
        private void doSingleClick(@NotNull final InputEvent evt, final int dot) {
            if ((evt.getModifiers() & InputEvent.SHIFT_MASK) == 0) {
                setCaretPosition(dot);
            } else {
                selection.setSelectionRectangular((evt.getModifiers() & InputEvent.CTRL_MASK) != 0);
                select(selection.getMarkPosition(), dot);
            }
        }
 
        private void doDoubleClick(final int line, final int offset, final int dot) {
            // Ignore empty lines
            if (selection.getLineLength(line) == 0) {
                return;
            }
 
            try {
                int bracket = TextUtilities.findMatchingBracket(document, Math.max(0, dot - 1));
                if (bracket != -1) {
                    int mark = selection.getMarkPosition();
                    // Hack
                    if (bracket > mark) {
                        bracket++;
                        mark--;
                    }
                    select(mark, bracket);
                    return;
                }
            } catch (final BadLocationException bl) {
                bl.printStackTrace();
            }
 
            // Ok, it's not a bracket... select the word
            final CharSequence lineText = selection.getLineText(line);
            char ch = lineText.charAt(Math.max(0, offset - 1));
 
            String noWordSep = (String) document.getProperty("noWordSep");
            if (noWordSep == null) {
                noWordSep = "";
            }
 
            // If the user clicked on a non-letter char,
            // we select the surrounding non-letters
            final boolean selectNoLetter = !Character.isLetterOrDigit(ch) && noWordSep.indexOf(ch) == -1;
 
            int wordStart = 0;
 
            for (int i = offset - 1; i >= 0; i--) {
                ch = lineText.charAt(i);
                if (selectNoLetter ^ (!Character.isLetterOrDigit(ch) && noWordSep.indexOf(ch) == -1)) {
                    wordStart = i + 1;
                    break;
                }
            }
 
            int wordEnd = lineText.length();
            for (int i = offset; i < lineText.length(); i++) {
                ch = lineText.charAt(i);
                if (selectNoLetter ^ (!Character.isLetterOrDigit(ch) && noWordSep.indexOf(ch) == -1)) {
                    wordEnd = i;
                    break;
                }
            }
 
            final int lineStart = selection.getLineStartOffset(line);
            select(lineStart + wordStart, lineStart + wordEnd);
 
            /*
            String lineText = getLineText(line);
            String noWordSep = (String)document.getProperty("noWordSep");
            int wordStart = TextUtilities.findWordStart(lineText, offset, noWordSep);
            int wordEnd = TextUtilities.findWordEnd(lineText, offset, noWordSep);
 
            int lineStart = getLineStartOffset(line);
            select(lineStart + wordStart, lineStart + wordEnd);
            */
        }
 
        private void doTripleClick(final int line) {
            select(selection.getLineStartOffset(line), selection.getLineEndOffset(line) - 1);
        }
 
    }
 
    private class CaretUndo extends AbstractUndoableEdit {
 
        private static final long serialVersionUID = 1L;
 
        private int start;
 
        private int end;
 
        private CaretUndo(final int start, final int end) {
            this.start = start;
            this.end = end;
        }
 
        @Override
        public boolean isSignificant() {
            return false;
        }
 
        @NotNull
        @Override
        public String getPresentationName() {
            return "caret move";
        }
 
        @Override
        public void undo() throws CannotUndoException {
            super.undo();
 
            select(start, end);
        }
 
        @Override
        public void redo() throws CannotRedoException {
            super.redo();
 
            select(start, end);
        }
 
        @Override
        public boolean addEdit(@NotNull final UndoableEdit anEdit) {
            if (anEdit instanceof CaretUndo) {
                final CaretUndo caretUndo = (CaretUndo) anEdit;
                start = caretUndo.start;
                end = caretUndo.end;
                caretUndo.die();
 
                return true;
            }
            return false;
        }
 
    }
 
}