0001: /*
0002: * JEditTextArea.java - jEdit's text component
0003: * Copyright (C) 1999 Slava Pestov
0004: *
0005: * You may use and modify this package for any purpose. Redistribution is
0006: * permitted, in both source and binary form, provided that this notice
0007: * remains intact in all source distributions of this package.
0008: */
0009: package workbench.gui.editor;
0010:
0011: import java.awt.AWTEvent;
0012: import java.awt.Color;
0013: import java.awt.Component;
0014: import java.awt.Container;
0015: import java.awt.Dimension;
0016: import java.awt.EventQueue;
0017: import java.awt.Font;
0018: import java.awt.FontMetrics;
0019: import java.awt.Insets;
0020: import java.awt.LayoutManager;
0021: import java.awt.Point;
0022: import java.awt.datatransfer.Clipboard;
0023: import java.awt.datatransfer.DataFlavor;
0024: import java.awt.datatransfer.StringSelection;
0025: import java.awt.event.ActionEvent;
0026: import java.awt.event.ActionListener;
0027: import java.awt.event.AdjustmentEvent;
0028: import java.awt.event.AdjustmentListener;
0029: import java.awt.event.ComponentAdapter;
0030: import java.awt.event.ComponentEvent;
0031: import java.awt.event.FocusEvent;
0032: import java.awt.event.FocusListener;
0033: import java.awt.event.InputEvent;
0034: import java.awt.event.KeyEvent;
0035: import java.awt.event.KeyListener;
0036: import java.awt.event.MouseAdapter;
0037: import java.awt.event.MouseEvent;
0038: import java.awt.event.MouseMotionListener;
0039: import java.awt.event.MouseWheelEvent;
0040: import java.awt.event.MouseWheelListener;
0041: import java.util.Enumeration;
0042: import java.util.Vector;
0043:
0044: import javax.swing.JComponent;
0045: import javax.swing.JPopupMenu;
0046: import javax.swing.JScrollBar;
0047: import javax.swing.KeyStroke;
0048: import javax.swing.Timer;
0049: import javax.swing.event.CaretEvent;
0050: import javax.swing.event.CaretListener;
0051: import javax.swing.event.DocumentEvent;
0052: import javax.swing.event.DocumentListener;
0053: import javax.swing.event.EventListenerList;
0054: import javax.swing.text.BadLocationException;
0055: import javax.swing.text.Element;
0056: import javax.swing.text.PlainDocument;
0057: import javax.swing.text.Segment;
0058: import javax.swing.text.Utilities;
0059: import javax.swing.undo.AbstractUndoableEdit;
0060: import javax.swing.undo.CannotRedoException;
0061: import javax.swing.undo.CannotUndoException;
0062: import javax.swing.undo.UndoableEdit;
0063:
0064: import workbench.gui.actions.WbAction;
0065: import workbench.gui.menu.TextPopup;
0066: import workbench.interfaces.ClipboardSupport;
0067: import workbench.interfaces.EditorStatusbar;
0068: import workbench.interfaces.TextChangeListener;
0069: import workbench.interfaces.TextSelectionListener;
0070: import workbench.interfaces.Undoable;
0071: import workbench.log.LogMgr;
0072: import workbench.resource.Settings;
0073: import workbench.util.NumberStringCache;
0074: import workbench.util.StringUtil;
0075:
0076: /**
0077: * jEdit's text area component. It is more suited for editing program
0078: * source code than JEditorPane, because it drops the unnecessary features
0079: * (images, variable-width lines, and so on) and adds a whole bunch of
0080: * useful goodies such as:
0081: * <ul>
0082: * <li>More flexible key binding scheme
0083: * <li>Supports macro recorders
0084: * <li>Rectangular selection
0085: * <li>Bracket highlighting
0086: * <li>Syntax highlighting
0087: * <li>Command repetition
0088: * <li>Block caret can be enabled
0089: * </ul>
0090: * It is also faster and doesn't have as many problems. It can be used
0091: * in other applications; the only other part of jEdit it depends on is
0092: * the syntax package.<p>
0093: *
0094: * To use it in your app, treat it like any other component, for example:
0095: * <pre>JEditTextArea ta = new JEditTextArea();
0096: * ta.setTokenMarker(new JavaTokenMarker());
0097: * ta.setText("public class Test {\n"
0098: * + " public static void main(String[] args) {\n"
0099: * + " System.out.println(\"Hello World\");\n"
0100: * + " }\n"
0101: * + "}");</pre>
0102: *
0103: * @author Slava Pestov
0104: */
0105: public class JEditTextArea extends JComponent implements
0106: MouseWheelListener, Undoable, ClipboardSupport, FocusListener {
0107: protected boolean rightClickMovesCursor = false;
0108:
0109: private Color alternateSelectionColor;
0110: private static final Color ERROR_COLOR = Color.RED.brighter();
0111: private static final Color TEMP_COLOR = Color.GREEN.brighter();
0112: private boolean currentSelectionIsTemporary;
0113: protected String commentChar;
0114: private TokenMarker currentTokenMarker;
0115:
0116: private KeyListener keyEventInterceptor;
0117: private EditorStatusbar statusBar;
0118:
0119: protected static final String CENTER = "center";
0120: protected static final String RIGHT = "right";
0121: protected static final String BOTTOM = "bottom";
0122:
0123: protected Timer caretTimer;
0124:
0125: protected TextAreaPainter painter;
0126:
0127: protected TextPopup popup;
0128:
0129: protected EventListenerList listeners;
0130: protected MutableCaretEvent caretEvent;
0131:
0132: protected boolean caretBlinks;
0133: protected boolean caretVisible;
0134: protected boolean blink;
0135:
0136: protected boolean editable;
0137: protected boolean autoIndent;
0138:
0139: protected int firstLine;
0140: protected int visibleLines;
0141: protected int electricScroll;
0142:
0143: protected int horizontalOffset;
0144:
0145: protected JScrollBar vertical;
0146: protected JScrollBar horizontal;
0147: protected boolean scrollBarsInitialized;
0148:
0149: protected InputHandler inputHandler;
0150: protected SyntaxDocument document;
0151: protected DocumentHandler documentHandler;
0152:
0153: protected Segment lineSegment;
0154:
0155: protected int selectionStart;
0156: protected int selectionStartLine;
0157: protected int selectionEnd;
0158: protected int selectionEndLine;
0159: protected boolean biasLeft;
0160: protected Color currentColor = null;
0161:
0162: protected int bracketPosition;
0163: protected int bracketLine;
0164:
0165: protected int magicCaret;
0166: protected boolean overwrite;
0167: protected boolean rectSelect;
0168: protected boolean modified;
0169:
0170: private int invalidationInterval = 10;
0171:
0172: /**
0173: * Creates a new JEditTextArea with the default settings.
0174: */
0175: public JEditTextArea() {
0176: // Enable the necessary events
0177: enableEvents(AWTEvent.KEY_EVENT_MASK);
0178:
0179: painter = new TextAreaPainter(this );
0180: setBackground(Color.WHITE);
0181:
0182: documentHandler = new DocumentHandler();
0183: listeners = new EventListenerList();
0184: caretEvent = new MutableCaretEvent();
0185: lineSegment = new Segment();
0186: bracketLine = bracketPosition = -1;
0187: blink = true;
0188:
0189: // Initialize the GUI
0190: setLayout(new ScrollLayout());
0191: add(CENTER, painter);
0192: add(RIGHT, vertical = new JScrollBar(JScrollBar.VERTICAL));
0193: add(BOTTOM, horizontal = new JScrollBar(JScrollBar.HORIZONTAL));
0194:
0195: // Add some event listeners
0196: vertical.addAdjustmentListener(new AdjustHandler());
0197: horizontal.addAdjustmentListener(new AdjustHandler());
0198: painter.addComponentListener(new ComponentHandler());
0199: painter.addMouseListener(new MouseHandler());
0200: painter.addMouseMotionListener(new DragHandler());
0201: this .addMouseWheelListener(this );
0202: addFocusListener(this );
0203:
0204: // Load the defaults
0205: setInputHandler(new DefaultInputHandler());
0206: this .inputHandler.addDefaultKeyBindings();
0207: setDocument(new SyntaxDocument());
0208: editable = true;
0209:
0210: // Let the focusGained() event display the caret
0211: caretVisible = false;
0212: caretBlinks = true;
0213:
0214: electricScroll = Settings.getInstance().getElectricScroll();
0215: autoIndent = true;
0216: this .setTabSize(Settings.getInstance().getEditorTabWidth());
0217: this .popup = new TextPopup(this );
0218:
0219: this .addKeyBinding("C+C", this .popup.getCopyAction());
0220: this .addKeyBinding("C+INSERT", this .popup.getCopyAction());
0221:
0222: this .addKeyBinding("C+V", this .popup.getPasteAction());
0223: this .addKeyBinding("SHIFT+INSERT", this .popup.getPasteAction());
0224:
0225: this .addKeyBinding("C+X", this .popup.getCutAction());
0226: this .addKeyBinding("SHIFT+DELETE", this .popup.getCutAction());
0227:
0228: this .addKeyBinding("C+a", this .popup.getSelectAllAction());
0229: this .invalidationInterval = Settings.getInstance()
0230: .getIntProperty("workbench.editor.update.lineinterval",
0231: 10);
0232: }
0233:
0234: public int getHScrollBarHeight() {
0235: if (horizontal != null && horizontal.isVisible())
0236: return (int) horizontal.getPreferredSize().getHeight();
0237: else
0238: return 0;
0239: }
0240:
0241: public Point getCursorLocation() {
0242: int line = getCaretLine();
0243: int pos = getCaretPosition() - getLineStartOffset(line);
0244: FontMetrics fm = painter.getFontMetrics();
0245: int y = (line - firstLine + 1) * fm.getHeight();
0246: if (y <= 0)
0247: y = 0;
0248: y += 4;
0249: int x = offsetToX(line, pos);
0250: if (x < 0)
0251: x = 0;
0252: x += this .getPainter().getGutterWidth();
0253: return new Point(x, y);
0254: }
0255:
0256: public void setShowLineNumbers(boolean aFlag) {
0257: this .painter.setShowLineNumbers(aFlag);
0258: }
0259:
0260: public boolean getShowLineNumbers() {
0261: return this .painter.getShowLineNumbers();
0262: }
0263:
0264: private String fixLinefeed(String input) {
0265: return StringUtil.makePlainLinefeed(input);
0266: }
0267:
0268: private void changeCase(boolean toLower) {
0269: String sel = this .getSelectedText();
0270: if (sel == null || sel.length() == 0)
0271: return;
0272: int start = this .getSelectionStart();
0273: int end = this .getSelectionEnd();
0274: if (toLower)
0275: sel = sel.toLowerCase();
0276: else
0277: sel = sel.toUpperCase();
0278: this .setSelectedText(sel);
0279: this .select(start, end);
0280: }
0281:
0282: public String getCommentChar() {
0283: return this .commentChar;
0284: }
0285:
0286: public void toLowerCase() {
0287: this .changeCase(true);
0288: }
0289:
0290: public void toUpperCase() {
0291: this .changeCase(false);
0292: }
0293:
0294: public void matchBracket() {
0295: try {
0296: int bracket = getBracketPosition() + 1;
0297: int line = getBracketLine();
0298: int caret = getLineStartOffset(line) + bracket;
0299: if (caret > -1) {
0300: scrollTo(line, caret);
0301: setCaretPosition(caret);
0302: }
0303: } catch (Exception e) {
0304: // ignore
0305: }
0306: }
0307:
0308: public void addKeyBinding(String aBinding, ActionListener aListener) {
0309: this .getInputHandler().addKeyBinding(aBinding, aListener);
0310: }
0311:
0312: public void addKeyBinding(WbAction anAction) {
0313: KeyStroke key = anAction.getAccelerator();
0314: if (key != null) {
0315: this .getInputHandler().addKeyBinding(key, anAction);
0316: }
0317: }
0318:
0319: public void removeKeyBinding(KeyStroke key) {
0320: this .getInputHandler().removeKeyBinding(key);
0321: }
0322:
0323: @SuppressWarnings("deprecation")
0324: public final boolean isManagingFocus() {
0325: return true;
0326: }
0327:
0328: /**
0329: * Returns the object responsible for painting this text area.
0330: */
0331: public final TextAreaPainter getPainter() {
0332: return painter;
0333: }
0334:
0335: /**
0336: * Returns the input handler.
0337: */
0338: public final InputHandler getInputHandler() {
0339: return inputHandler;
0340: }
0341:
0342: /**
0343: * Sets the input handler.
0344: * @param inputHandler The new input handler
0345: */
0346: public void setInputHandler(InputHandler inputHandler) {
0347: this .inputHandler = inputHandler;
0348: }
0349:
0350: /**
0351: * Returns true if the caret is blinking, false otherwise.
0352: */
0353: public final boolean isCaretBlinkEnabled() {
0354: return caretBlinks;
0355: }
0356:
0357: protected void stopBlinkTimer() {
0358: if (this .caretTimer != null) {
0359: caretTimer.stop();
0360: }
0361: caretTimer = null;
0362: }
0363:
0364: private void startBlinkTimer() {
0365: if (caretTimer != null)
0366: return;
0367:
0368: final int blinkInterval = 750;
0369: caretTimer = new Timer(blinkInterval, new ActionListener() {
0370: public void actionPerformed(ActionEvent evt) {
0371: blinkCaret();
0372: }
0373: });
0374: caretTimer.setInitialDelay(blinkInterval);
0375: caretTimer.start();
0376: }
0377:
0378: /**
0379: * Toggles caret blinking.
0380: * @param caretBlinks True if the caret should blink, false otherwise
0381: */
0382: public void setCaretBlinkEnabled(boolean caretBlinks) {
0383: this .caretBlinks = caretBlinks;
0384: if (!caretBlinks) {
0385: blink = false;
0386: }
0387: if (caretBlinks) {
0388: startBlinkTimer();
0389: } else {
0390: stopBlinkTimer();
0391: }
0392: painter.invalidateSelectedLines();
0393: }
0394:
0395: /**
0396: * Returns true if the caret is visible, false otherwise.
0397: */
0398: public final boolean isCaretVisible() {
0399: return (!caretBlinks || blink) && caretVisible;
0400: }
0401:
0402: public boolean isTextSelected() {
0403: int start = this .getSelectionStart();
0404: int end = this .getSelectionEnd();
0405: return (start < end);
0406: }
0407:
0408: /**
0409: * Sets if the caret should be visible.
0410: * @param caretVisible True if the caret should be visible, false
0411: * otherwise
0412: */
0413: public void setCaretVisible(boolean caretVisible) {
0414: this .caretVisible = caretVisible;
0415: blink = true;
0416: painter.invalidateSelectedLines();
0417: }
0418:
0419: public void focusGained(FocusEvent e) {
0420: setCaretVisible(true);
0421: }
0422:
0423: public void focusLost(FocusEvent e) {
0424: setCaretVisible(false);
0425: }
0426:
0427: /**
0428: * Blinks the caret.
0429: */
0430: public final void blinkCaret() {
0431: if (!caretVisible)
0432: return;
0433:
0434: if (caretBlinks) {
0435: blink = !blink;
0436: painter.invalidateSelectedLines();
0437: } else {
0438: blink = true;
0439: }
0440: }
0441:
0442: /**
0443: * Returns the number of lines from the top and button of the
0444: * text area that are always visible.
0445: */
0446: public final int getElectricScroll() {
0447: return electricScroll;
0448: }
0449:
0450: /**
0451: * Sets the number of lines from the top and bottom of the text
0452: * area that are always visible
0453: * @param electricScroll The number of lines always visible from
0454: * the top or bottom
0455: */
0456: public final void setElectricScroll(int electricScroll) {
0457: this .electricScroll = electricScroll;
0458: }
0459:
0460: /**
0461: * Updates the state of the scroll bars. This should be called
0462: * if the number of lines in the document changes, or when the
0463: * size of the text area changes.
0464: */
0465: public void updateScrollBars() {
0466: if (vertical != null && visibleLines != 0) {
0467: vertical.setValues(firstLine, visibleLines, 0,
0468: getLineCount());
0469: vertical.setUnitIncrement(2);
0470: vertical.setBlockIncrement(visibleLines);
0471: if (visibleLines > getLineCount()) {
0472: setFirstLine(0);
0473: }
0474: }
0475:
0476: int charWidth = painter.getFontMetrics().charWidth('w');
0477: int maxLineLength = getDocument().getMaxLineLength();
0478: int maxLineWidth = (charWidth * maxLineLength)
0479: + this .painter.getGutterWidth() + 10;
0480: int width = painter.getWidth();
0481: if (horizontal != null && width != 0) {
0482: horizontal.setValues(-horizontalOffset, width, 0,
0483: maxLineWidth);
0484: horizontal.setUnitIncrement(charWidth);
0485: horizontal.setBlockIncrement(width / 3);
0486: }
0487: }
0488:
0489: /**
0490: * Returns the line displayed at the text area's origin.
0491: */
0492: public final int getFirstLine() {
0493: return (firstLine < 0 ? 0 : firstLine);
0494: }
0495:
0496: /**
0497: * Sets the line displayed at the text area's origin without
0498: * updating the scroll bars.
0499: */
0500: public void setFirstLine(int firstLine) {
0501: if (firstLine == this .firstLine)
0502: return;
0503: this .firstLine = firstLine;
0504:
0505: if (firstLine != vertical.getValue()) {
0506: updateScrollBars();
0507: }
0508:
0509: painter.repaint();
0510: }
0511:
0512: /**
0513: * Returns the number of lines visible in this text area.
0514: */
0515: public final int getVisibleLines() {
0516: return visibleLines;
0517: }
0518:
0519: /**
0520: * Recalculates the number of visible lines. This should not
0521: * be called directly.
0522: */
0523: final void recalculateVisibleLines() {
0524: if (painter == null) {
0525: return;
0526: }
0527: int height = painter.getHeight();
0528: int lineHeight = painter.getFontMetrics().getHeight();
0529: visibleLines = height / lineHeight;
0530: updateScrollBars();
0531: }
0532:
0533: /**
0534: * Returns the horizontal offset of drawn lines.
0535: */
0536: public final int getHorizontalOffset() {
0537: return horizontalOffset;
0538: }
0539:
0540: /**
0541: * Sets the horizontal offset of drawn lines. This can be used to
0542: * implement horizontal scrolling.
0543: * @param horizontalOffset offset The new horizontal offset
0544: */
0545: public void setHorizontalOffset(int horizontalOffset) {
0546: if (horizontalOffset == this .horizontalOffset)
0547: return;
0548: this .horizontalOffset = horizontalOffset;
0549: if (horizontal != null
0550: && horizontalOffset != horizontal.getValue())
0551: updateScrollBars();
0552: painter.repaint();
0553: }
0554:
0555: /**
0556: * A fast way of changing both the first line and horizontal
0557: * offset.
0558: * @param firstLine The new first line
0559: * @param horizontalOffset The new horizontal offset
0560: * @return True if any of the values were changed, false otherwise
0561: */
0562: public boolean setOrigin(int firstLine, int horizontalOffset) {
0563: boolean changed = false;
0564:
0565: if (horizontalOffset != this .horizontalOffset) {
0566: this .horizontalOffset = horizontalOffset;
0567: changed = true;
0568: }
0569:
0570: if (firstLine != this .firstLine) {
0571: this .firstLine = firstLine;
0572: changed = true;
0573: }
0574:
0575: if (changed) {
0576: updateScrollBars();
0577: painter.repaint();
0578: }
0579:
0580: return changed;
0581: }
0582:
0583: /**
0584: * Ensures that the caret is visible by scrolling the text area if
0585: * necessary.
0586: * @return True if scrolling was actually performed, false if the
0587: * caret was already visible
0588: */
0589: public boolean scrollToCaret() {
0590: int line = getCaretLine();
0591: int lineStart = getLineStartOffset(line);
0592: int offset = Math.max(0, Math.min(getLineLength(line) - 1,
0593: getCaretPosition() - lineStart));
0594:
0595: return scrollTo(line, offset);
0596: }
0597:
0598: /**
0599: * Ensures that the specified line and offset is visible by scrolling
0600: * the text area if necessary.
0601: * @param line The line to scroll to
0602: * @param offset The offset in the line to scroll to
0603: * @return True if scrolling was actually performed, false if the
0604: * line and offset was already visible
0605: */
0606: public boolean scrollTo(final int line, final int offset) {
0607: if (visibleLines == 0) {
0608: // visibleLines == 0 before the component is realized
0609: // we can't do any proper scrolling, so we'll try again later
0610: EventQueue.invokeLater(new Runnable() {
0611: public void run() {
0612: scrollTo(line, offset);
0613: }
0614: });
0615: return false;
0616: }
0617:
0618: int newFirstLine = firstLine;
0619: int newHorizontalOffset = horizontalOffset;
0620: int lineCount = getLineCount();
0621:
0622: if (line < firstLine + electricScroll) {
0623: newFirstLine = Math.max(0, line - electricScroll);
0624: } else if (line + electricScroll >= firstLine + visibleLines) {
0625: newFirstLine = (line - visibleLines) + electricScroll + 1;
0626:
0627: if (newFirstLine + visibleLines >= lineCount) {
0628: newFirstLine = lineCount - visibleLines;
0629: }
0630: if (newFirstLine < 0) {
0631: newFirstLine = 0;
0632: }
0633: }
0634:
0635: int x = _offsetToX(line, offset);
0636: int width = painter.getFontMetrics().charWidth('w');
0637: int pwidth = painter.getWidth();
0638:
0639: if (x < 0) {
0640: newHorizontalOffset = Math.min(0, horizontalOffset - x
0641: + width + 5);
0642: } else if (x + width >= pwidth) {
0643: newHorizontalOffset = horizontalOffset + (pwidth - x)
0644: - width - 5;
0645: if (this .painter.getShowLineNumbers()) {
0646: newHorizontalOffset -= painter.getGutterWidth();
0647: }
0648: }
0649:
0650: return setOrigin(newFirstLine, newHorizontalOffset);
0651: }
0652:
0653: /**
0654: * Converts a line index to a y co-ordinate.
0655: * @param line The line
0656: */
0657: public int lineToY(int line) {
0658: FontMetrics fm = painter.getFontMetrics();
0659: return (line - firstLine) * fm.getHeight()
0660: - (fm.getLeading() + fm.getMaxDescent());
0661: }
0662:
0663: /**
0664: * Converts a y co-ordinate to a line index.
0665: * @param y The y co-ordinate
0666: */
0667: public int yToLine(int y) {
0668: FontMetrics fm = painter.getFontMetrics();
0669: int height = fm.getHeight();
0670: return Math.max(0, Math.min(getLineCount() - 1, y / height
0671: + firstLine));
0672: }
0673:
0674: /**
0675: * Converts an offset in a line into an x co-ordinate. This is a
0676: * slow version that can be used any time.
0677: * @param line The line
0678: * @param offset The offset, from the start of the line
0679: */
0680: public final int offsetToX(int line, int offset) {
0681: // don't use cached tokens
0682: painter.currentLineTokens = null;
0683: return _offsetToX(line, offset);
0684: }
0685:
0686: /**
0687: * Converts an offset in a line into an x co-ordinate. This is a
0688: * fast version that should only be used if no changes were made
0689: * to the text since the last repaint.
0690: * @param line The line
0691: * @param offset The offset, from the start of the line
0692: */
0693: public int _offsetToX(int line, int offset) {
0694: TokenMarker tokenMarker = getTokenMarker();
0695:
0696: /* Use painter's cached info for speed */
0697: FontMetrics fm = painter.getFontMetrics();
0698:
0699: getLineText(line, lineSegment);
0700:
0701: int segmentOffset = lineSegment.offset;
0702: int x = horizontalOffset;
0703:
0704: /* If syntax coloring is disabled, do simple translation */
0705: if (tokenMarker == null) {
0706: lineSegment.count = offset;
0707: return x
0708: + Utilities.getTabbedTextWidth(lineSegment, fm, x,
0709: painter, 0);
0710: } else {
0711: // If syntax coloring is enabled, we have to do this because
0712: // tokens can vary in width
0713: Token tokens = tokenMarker.markTokens(lineSegment, line);
0714:
0715: Font defaultFont = painter.getFont();
0716: SyntaxStyle[] styles = painter.getStyles();
0717:
0718: while (tokens != null) {
0719: byte id = tokens.id;
0720:
0721: if (id == Token.NULL) {
0722: fm = painter.getFontMetrics();
0723: } else {
0724: fm = styles[id].getFontMetrics(defaultFont);
0725: }
0726: int length = tokens.length;
0727:
0728: if (offset + segmentOffset < lineSegment.offset
0729: + length) {
0730: lineSegment.count = offset
0731: - (lineSegment.offset - segmentOffset);
0732: return x
0733: + Utilities.getTabbedTextWidth(lineSegment,
0734: fm, x, painter, 0);
0735: } else {
0736: lineSegment.count = length;
0737: x += Utilities.getTabbedTextWidth(lineSegment, fm,
0738: x, painter, 0);
0739: lineSegment.offset += length;
0740: }
0741: tokens = tokens.next;
0742: }
0743: }
0744: return x;
0745: }
0746:
0747: /**
0748: * Converts an x co-ordinate to an offset within a line.
0749: * @param line The line
0750: * @param x The x co-ordinate
0751: */
0752: public int xToOffset(int line, int x) {
0753: TokenMarker tokenMarker = getTokenMarker();
0754:
0755: /* Use painter's cached info for speed */
0756: FontMetrics fm = painter.getFontMetrics();
0757:
0758: getLineText(line, lineSegment);
0759:
0760: char[] segmentArray = lineSegment.array;
0761: int segmentOffset = lineSegment.offset;
0762: int segmentCount = lineSegment.count;
0763:
0764: int width = horizontalOffset;
0765:
0766: if (tokenMarker == null) {
0767: for (int i = 0; i < segmentCount; i++) {
0768: char c = segmentArray[i + segmentOffset];
0769: int charWidth;
0770:
0771: if (c == '\t') {
0772: charWidth = (int) painter.nextTabStop(width, i)
0773: - width;
0774: } else {
0775: charWidth = fm.charWidth(c);
0776: }
0777: if (x - charWidth / 2 <= width) {
0778: return i;
0779: }
0780: width += charWidth;
0781: }
0782:
0783: return segmentCount;
0784: } else {
0785: Token tokens = tokenMarker.markTokens(lineSegment, line);
0786:
0787: int offset = 0;
0788: Font defaultFont = painter.getFont();
0789: SyntaxStyle[] styles = painter.getStyles();
0790:
0791: while (tokens != null) {
0792: byte id = tokens.id;
0793:
0794: if (id == Token.NULL) {
0795: fm = painter.getFontMetrics();
0796: } else {
0797: fm = styles[id].getFontMetrics(defaultFont);
0798: }
0799:
0800: int length = tokens.length;
0801:
0802: for (int i = 0; i < length; i++) {
0803: char c = segmentArray[segmentOffset + offset + i];
0804: int charWidth = fm.charWidth(c);
0805:
0806: if (c == '\t') {
0807: charWidth = (int) painter.nextTabStop(width,
0808: offset + i)
0809: - width;
0810: }
0811:
0812: if (x - charWidth / 2 <= width)
0813: return offset + i;
0814:
0815: width += charWidth;
0816: }
0817:
0818: offset += length;
0819: tokens = tokens.next;
0820: }
0821: return offset;
0822: }
0823:
0824: }
0825:
0826: /**
0827: * Converts a point to an offset, from the start of the text.
0828: * @param x The x co-ordinate of the point
0829: * @param y The y co-ordinate of the point
0830: */
0831: public int xyToOffset(int x, int y) {
0832: int line = yToLine(y);
0833: int start = getLineStartOffset(line);
0834: return start + xToOffset(line, x);
0835: }
0836:
0837: /**
0838: * Returns the document this text area is editing.
0839: */
0840: public final SyntaxDocument getDocument() {
0841: return document;
0842: }
0843:
0844: /**
0845: * Sets the document this text area is editing.
0846: * @param document The document
0847: */
0848: public void setDocument(SyntaxDocument document) {
0849: if (this .document == document)
0850: return;
0851:
0852: if (this .document != null) {
0853: this .document.removeDocumentListener(documentHandler);
0854: this .document.dispose();
0855: }
0856:
0857: this .document = document;
0858:
0859: if (this .document != null) {
0860: painter.calculateTabSize();
0861:
0862: if (this .currentTokenMarker != null) {
0863: this .document.setTokenMarker(this .currentTokenMarker);
0864: }
0865:
0866: this .document.addDocumentListener(documentHandler);
0867:
0868: EventQueue.invokeLater(new Runnable() {
0869: public void run() {
0870: painter.invalidateLineRange(0, getLineCount());
0871: //setCaretPosition(0);
0872: painter.repaint();
0873: painter.validate();
0874: repaint();
0875: validate();
0876: updateScrollBars();
0877: }
0878: });
0879: }
0880: }
0881:
0882: public void setFont(Font aNewFont) {
0883: super .setFont(aNewFont);
0884: this .painter.setFont(aNewFont);
0885: }
0886:
0887: /**
0888: * Returns the document's token marker. Equivalent to calling
0889: * <code>getDocument().getTokenMarker()</code>.
0890: */
0891: public final TokenMarker getTokenMarker() {
0892: return document.getTokenMarker();
0893: }
0894:
0895: /**
0896: * Sets the document's token marker. Equivalent to caling
0897: * <code>getDocument().setTokenMarker()</code>.
0898: * @param tokenMarker The token marker
0899: */
0900: public final void setTokenMarker(TokenMarker tokenMarker) {
0901: this .currentTokenMarker = tokenMarker;
0902: document.setTokenMarker(tokenMarker);
0903: }
0904:
0905: /**
0906: * Returns the length of the document. Equivalent to calling
0907: * <code>getDocument().getLength()</code>.
0908: */
0909: public final int getDocumentLength() {
0910: return document.getLength();
0911: }
0912:
0913: /**
0914: * Returns the number of lines in the document.
0915: */
0916: public final int getLineCount() {
0917: return document.getDefaultRootElement().getElementCount();
0918: }
0919:
0920: /**
0921: * Returns the line containing the specified offset.
0922: * @param offset The offset
0923: */
0924: public final int getLineOfOffset(int offset) {
0925: return document.getDefaultRootElement().getElementIndex(offset);
0926: }
0927:
0928: public int getCaretPositionInLine(int line) {
0929: int pos = getCaretPosition();
0930: int start = getLineStartOffset(line);
0931: return (pos - start);
0932:
0933: }
0934:
0935: /**
0936: * Returns the start offset of the specified line.
0937: * @param line The line
0938: * @return The start offset of the specified line, or -1 if the line is
0939: * invalid
0940: */
0941: public int getLineStartOffset(int line) {
0942: Element lineElement = document.getDefaultRootElement()
0943: .getElement(line);
0944: if (lineElement == null)
0945: return -1;
0946: else
0947: return lineElement.getStartOffset();
0948: }
0949:
0950: /**
0951: * Returns the end offset of the specified line.
0952: * @param line The line
0953: * @return The end offset of the specified line, or -1 if the line is
0954: * invalid.
0955: */
0956: public int getLineEndOffset(int line) {
0957: Element lineElement = document.getDefaultRootElement()
0958: .getElement(line);
0959: if (lineElement == null)
0960: return -1;
0961: else
0962: return lineElement.getEndOffset();
0963: }
0964:
0965: /**
0966: * Returns the length of the specified line, without the line end terminator
0967: * @param line The line
0968: */
0969: public int getLineLength(int line) {
0970: Element lineElement = document.getDefaultRootElement()
0971: .getElement(line);
0972:
0973: if (lineElement == null)
0974: return -1;
0975: else
0976: return lineElement.getEndOffset()
0977: - lineElement.getStartOffset() - 1;
0978: }
0979:
0980: /**
0981: * Returns the entire text of this text area.
0982: */
0983: public String getText() {
0984: int len = document.getLength();
0985: if (len < 0)
0986: return null;
0987: try {
0988: return document.getText(0, document.getLength());
0989: } catch (BadLocationException bl) {
0990: LogMgr.logError("JEditTextArea.getText()",
0991: "Error setting text", bl);
0992: return null;
0993: }
0994: }
0995:
0996: /**
0997: * Set the tab size to be used in characters.
0998: */
0999: public void setTabSize(int aSize) {
1000: document.putProperty(PlainDocument.tabSizeAttribute,
1001: new Integer(aSize));
1002: }
1003:
1004: /**
1005: * Return the current Tab size in characters
1006: */
1007: public int getTabSize() {
1008: Integer tab = (Integer) document
1009: .getProperty(PlainDocument.tabSizeAttribute);
1010:
1011: if (tab != null) {
1012: return tab.intValue();
1013: } else {
1014: return 4;
1015: }
1016:
1017: }
1018:
1019: public void appendLine(String aLine) {
1020: try {
1021: document.beginCompoundEdit();
1022: document.insertString(document.getLength(),
1023: fixLinefeed(aLine), null);
1024: } catch (BadLocationException bl) {
1025: LogMgr.logError("JEditTextArea.appendLine()",
1026: "Error setting text", bl);
1027: } finally {
1028: document.endCompoundEdit();
1029: }
1030: }
1031:
1032: public void reset() {
1033: setText("");
1034: resetModified();
1035: }
1036:
1037: /**
1038: * Sets the entire text of this text area.
1039: */
1040: public void setText(String text) {
1041: try {
1042: document.beginCompoundEdit();
1043:
1044: if (document.getLength() > 0) {
1045: document.remove(0, document.getLength());
1046: }
1047: if (text != null && text.length() > 0) {
1048: String realtext = fixLinefeed(text);
1049: document.insertString(0, realtext, null);
1050: }
1051: } catch (BadLocationException bl) {
1052: LogMgr.logError("JEditTextArea.setText()",
1053: "Error setting text", bl);
1054: } finally {
1055: document.endCompoundEdit();
1056: document.tokenizeLines();
1057: }
1058:
1059: EventQueue.invokeLater(new Runnable() {
1060: public void run() {
1061: updateScrollBars();
1062: painter.invalidateLineRange(0, getLineCount());
1063: repaint();
1064: }
1065: });
1066: }
1067:
1068: /**
1069: * Returns the specified substring of the document.
1070: * @param start The start offset
1071: * @param len The length of the substring
1072: * @return The substring, or null if the offsets are invalid
1073: */
1074: public final String getText(int start, int len) {
1075: try {
1076: return document.getText(start, len);
1077: } catch (BadLocationException bl) {
1078: LogMgr.logError("JEditTextArea.getText()",
1079: "Error setting text", bl);
1080: return null;
1081: }
1082: }
1083:
1084: /**
1085: * Copies the specified substring of the document into a segment.
1086: * If the offsets are invalid, the segment will contain a null string.
1087: * @param start The start offset
1088: * @param len The length of the substring
1089: * @param segment The segment
1090: */
1091: public final void getText(int start, int len, Segment segment) {
1092: if (len < 0)
1093: return;
1094: try {
1095: document.getText(start, len, segment);
1096: } catch (BadLocationException bl) {
1097: LogMgr.logError("JEditTextArea.getText()",
1098: "Error setting text", bl);
1099: segment.offset = segment.count = 0;
1100: }
1101: }
1102:
1103: /**
1104: * Returns the word that is left of the cursor.
1105: * If the character left of the cursor is a whitespace
1106: * this method returns null.
1107: * @param wordBoundaries additional word boundary characters (whitespace is always a word boundary)
1108: */
1109: public String getWordAtCursor(String wordBoundaries) {
1110: int currentLine = getCaretLine();
1111: String line = this .getLineText(currentLine);
1112: int pos = this .getCaretPositionInLine(currentLine);
1113: return StringUtil
1114: .getWordLeftOfCursor(line, pos, wordBoundaries);
1115: }
1116:
1117: public void selectWordAtCursor(String wordBoundaries) {
1118: int currentLine = getCaretLine();
1119: String line = this .getLineText(currentLine);
1120: int caret = this .getCaretPosition();
1121: int lineStart = this .getLineStartOffset(currentLine);
1122: int pos = (caret - lineStart);
1123: //this.getCaretPositionInLine(currentLine);
1124: if (pos <= 0)
1125: return;
1126: if (Character.isWhitespace(line.charAt(pos - 1)))
1127: return;
1128: int start = StringUtil.findWordBoundary(line, pos - 1,
1129: wordBoundaries);
1130: if (start > -1) {
1131: this .select(lineStart + start + 1, caret);
1132: }
1133: }
1134:
1135: /**
1136: * Returns the text on the specified line without the line terminator
1137: * @param lineIndex The line
1138: * @return The text, or null if the line is invalid
1139: */
1140: public final String getLineText(int lineIndex) {
1141: Element lineElement = document.getDefaultRootElement()
1142: .getElement(lineIndex);
1143: int start = (lineElement != null ? lineElement.getStartOffset()
1144: : -1);
1145: int end = (lineElement != null ? lineElement.getEndOffset()
1146: : -1);
1147: return getText(start, end - start - 1);
1148: }
1149:
1150: /**
1151: * Copies the text on the specified line into a segment. If the line
1152: * is invalid, the segment will contain a null string.
1153: * @param lineIndex The line
1154: */
1155: public final void getLineText(int lineIndex, Segment segment) {
1156: Element lineElement = document.getDefaultRootElement()
1157: .getElement(lineIndex);
1158: int start = (lineElement != null ? lineElement.getStartOffset()
1159: : -1);
1160: int end = (lineElement != null ? lineElement.getEndOffset()
1161: : -1);
1162: getText(start, end - start - 1, segment);
1163: }
1164:
1165: /**
1166: * Returns the selection start offset.
1167: */
1168: public final int getSelectionStart() {
1169: return selectionStart;
1170: }
1171:
1172: /**
1173: * Returns the offset where the selection starts on the specified
1174: * line.
1175: */
1176: public int getSelectionStart(int line) {
1177: if (line == selectionStartLine) {
1178: return selectionStart;
1179: } else if (rectSelect) {
1180: Element map = document.getDefaultRootElement();
1181: int start = selectionStart
1182: - map.getElement(selectionStartLine)
1183: .getStartOffset();
1184:
1185: Element lineElement = map.getElement(line);
1186: int lineStart = lineElement.getStartOffset();
1187: int lineEnd = lineElement.getEndOffset() - 1;
1188: return Math.min(lineEnd, lineStart + start);
1189: } else {
1190: return getLineStartOffset(line);
1191: }
1192: }
1193:
1194: /**
1195: * Returns the selection start line.
1196: */
1197: public final int getSelectionStartLine() {
1198: return selectionStartLine;
1199: }
1200:
1201: /**
1202: * Sets the selection start. The new selection will be the new
1203: * selection start and the old selection end.
1204: * @param selectionStart The selection start
1205: * @see #select(int,int)
1206: */
1207: public final void setSelectionStart(int selectionStart) {
1208: select(selectionStart, selectionEnd);
1209: }
1210:
1211: /**
1212: * Returns the selection end offset.
1213: */
1214: public final int getSelectionEnd() {
1215: return selectionEnd;
1216: }
1217:
1218: /**
1219: * Returns the offset where the selection ends on the specified
1220: * line.
1221: */
1222: public int getSelectionEnd(int line) {
1223: if (line == selectionEndLine) {
1224: return selectionEnd;
1225: } else if (rectSelect) {
1226: Element map = document.getDefaultRootElement();
1227: int end = selectionEnd
1228: - map.getElement(selectionEndLine).getStartOffset();
1229:
1230: Element lineElement = map.getElement(line);
1231: int lineStart = lineElement.getStartOffset();
1232: int lineEnd = lineElement.getEndOffset() - 1;
1233: return Math.min(lineEnd, lineStart + end);
1234: } else {
1235: return getLineEndOffset(line) - 1;
1236: }
1237: }
1238:
1239: /**
1240: * Returns the selection end line.
1241: */
1242: public final int getSelectionEndLine() {
1243: return selectionEndLine;
1244: }
1245:
1246: /**
1247: * Sets the selection end. The new selection will be the old
1248: * selection start and the bew selection end.
1249: * @param selectionEnd The selection end
1250: * @see #select(int,int)
1251: */
1252: public final void setSelectionEnd(int selectionEnd) {
1253: select(selectionStart, selectionEnd);
1254: }
1255:
1256: /**
1257: * Returns the caret position. This will either be the selection
1258: * start or the selection end, depending on which direction the
1259: * selection was made in.
1260: */
1261: public final int getCaretPosition() {
1262: return (biasLeft ? selectionStart : selectionEnd);
1263: }
1264:
1265: /**
1266: * Returns the caret line.
1267: */
1268: public final int getCaretLine() {
1269: return (biasLeft ? selectionStartLine : selectionEndLine);
1270: }
1271:
1272: /**
1273: * Returns the mark position. This will be the opposite selection
1274: * bound to the caret position.
1275: * @see #getCaretPosition()
1276: */
1277: public final int getMarkPosition() {
1278: return (biasLeft ? selectionEnd : selectionStart);
1279: }
1280:
1281: /**
1282: * Returns the mark line.
1283: */
1284: public final int getMarkLine() {
1285: return (biasLeft ? selectionEndLine : selectionStartLine);
1286: }
1287:
1288: /**
1289: * Sets the caret position. The new selection will consist of the
1290: * caret position only (hence no text will be selected)
1291: * @param caret The caret position
1292: * @see #select(int,int)
1293: */
1294: public final void setCaretPosition(int caret) {
1295: select(caret, caret);
1296: }
1297:
1298: /**
1299: * Selects all text in the document.
1300: */
1301: public final void selectAll() {
1302: select(0, getDocumentLength());
1303: EventQueue.invokeLater(new Runnable() {
1304: public void run() {
1305: requestFocusInWindow();
1306: }
1307: });
1308: }
1309:
1310: /**
1311: * Moves the mark to the caret position.
1312: */
1313: public final void selectNone() {
1314: select(getCaretPosition(), getCaretPosition());
1315: }
1316:
1317: public void clearUndoBuffer() {
1318: this .document.clearUndoBuffer();
1319: }
1320:
1321: public void undo() {
1322: this .document.undo();
1323: int pos = this .document.getPositionOfLastChange();
1324: if (pos > -1) {
1325: this .setCaretPosition(pos);
1326: this .scrollToCaret();
1327: }
1328: }
1329:
1330: public void redo() {
1331: this .document.redo();
1332: int pos = this .document.getPositionOfLastChange();
1333: if (pos > -1) {
1334: this .setCaretPosition(pos);
1335: this .scrollToCaret();
1336: }
1337: }
1338:
1339: public boolean currentSelectionIsTemporary() {
1340: return currentSelectionIsTemporary;
1341: }
1342:
1343: public void selectError(int start, int end) {
1344: this .selectCommand(start, end, ERROR_COLOR);
1345: }
1346:
1347: public void selectStatementTemporary(int start, int end) {
1348: this .selectCommand(start, end, TEMP_COLOR);
1349: }
1350:
1351: private void selectCommand(int start, int end, Color alternateColor) {
1352: if (start >= end)
1353: return;
1354:
1355: int len = (end - start);
1356: String text = this .getText(start, len);
1357: if (text == null || text.length() == 0)
1358: return;
1359:
1360: len = text.length();
1361: int pos = 0;
1362: char c = text.charAt(pos);
1363: while (Character.isWhitespace(c) && pos < len) {
1364: pos++;
1365: c = text.charAt(pos);
1366: }
1367:
1368: int newStart = start + pos;
1369: int maxIndex = len - 1;
1370:
1371: pos = 0;
1372: c = text.charAt(maxIndex - pos);
1373: while (Character.isWhitespace(c) && pos < maxIndex) {
1374: pos++;
1375: c = text.charAt(maxIndex - pos);
1376: }
1377: int newEnd = end - pos;
1378: this .select(newStart, newEnd, alternateColor);
1379: }
1380:
1381: public void select(int start, int end) {
1382: this .select(start, end, null);
1383: }
1384:
1385: /**
1386: * Selects from the start offset to the end offset. This is the
1387: * general selection method used by all other selecting methods.
1388: * The caret position will be start if start < end, and end
1389: * if end > start.
1390: * @param start The start offset
1391: * @param end The end offset
1392: */
1393: private void select(int start, int end, Color alternateColor) {
1394: int newStart, newEnd;
1395: boolean newBias;
1396:
1397: if (start <= end) {
1398: newStart = start;
1399: newEnd = end;
1400: newBias = false;
1401: } else {
1402: newStart = end;
1403: newEnd = start;
1404: newBias = true;
1405: }
1406:
1407: if (newStart < 0 || newEnd > getDocumentLength()) {
1408: throw new IllegalArgumentException("Bounds out of"
1409: + " range: " + newStart + "," + newEnd);
1410: }
1411:
1412: // If the new position is the same as the old, we don't
1413: // do all this crap, however we still do the stuff at
1414: // the end (clearing magic position, scrolling)
1415: if (newStart != selectionStart || newEnd != selectionEnd
1416: || newBias != biasLeft) {
1417: this .alternateSelectionColor = alternateColor;
1418: this .currentSelectionIsTemporary = (alternateColor != null);
1419:
1420: int newStartLine = getLineOfOffset(newStart);
1421: int newEndLine = getLineOfOffset(newEnd);
1422:
1423: if (painter.isBracketHighlightEnabled()) {
1424: if (bracketLine != -1)
1425: painter.invalidateLine(bracketLine);
1426: updateBracketHighlight(end);
1427: if (bracketLine != -1)
1428: painter.invalidateLine(bracketLine);
1429: }
1430:
1431: painter.invalidateLineRange(selectionStartLine,
1432: selectionEndLine);
1433: painter.invalidateLineRange(newStartLine, newEndLine);
1434:
1435: document.addUndoableEdit(new CaretUndo(selectionStart,
1436: selectionEnd));
1437:
1438: selectionStart = newStart;
1439: selectionEnd = newEnd;
1440: selectionStartLine = newStartLine;
1441: selectionEndLine = newEndLine;
1442: biasLeft = newBias;
1443:
1444: fireCaretEvent();
1445: }
1446:
1447: // When the user is typing, etc, we don't want the caret
1448: // to blink
1449: blink = true;
1450: if (caretTimer != null)
1451: caretTimer.restart();
1452:
1453: // Disable rectangle select if selection start = selection end
1454: if (selectionStart == selectionEnd)
1455: rectSelect = false;
1456:
1457: // Clear the `magic' caret position used by up/down
1458: magicCaret = -1;
1459:
1460: scrollToCaret();
1461: fireSelectionEvent();
1462: }
1463:
1464: public Color getAlternateSelectionColor() {
1465: return this .alternateSelectionColor;
1466: }
1467:
1468: /**
1469: * Returns the selected text, or null if no selection is active.
1470: */
1471: public final String getSelectedText() {
1472: if (selectionStart == selectionEnd)
1473: return null;
1474:
1475: if (rectSelect) {
1476: // Return each row of the selection on a new line
1477: Element map = document.getDefaultRootElement();
1478:
1479: int start = selectionStart
1480: - map.getElement(selectionStartLine)
1481: .getStartOffset();
1482: int end = selectionEnd
1483: - map.getElement(selectionEndLine).getStartOffset();
1484:
1485: // Certain rectangles satisfy this condition...
1486: if (end < start) {
1487: int tmp = end;
1488: end = start;
1489: start = tmp;
1490: }
1491:
1492: StringBuilder buf = new StringBuilder();
1493: Segment seg = new Segment();
1494:
1495: for (int i = selectionStartLine; i <= selectionEndLine; i++) {
1496: Element lineElement = map.getElement(i);
1497: int lineStart = lineElement.getStartOffset();
1498: int lineEnd = lineElement.getEndOffset() - 1;
1499: int lineLen = lineEnd - lineStart;
1500:
1501: lineStart = Math.min(lineStart + start, lineEnd);
1502: lineLen = Math.min(end - start, lineEnd - lineStart);
1503:
1504: getText(lineStart, lineLen, seg);
1505: buf.append(seg.array, seg.offset, seg.count);
1506:
1507: if (i != selectionEndLine)
1508: buf.append('\n');
1509: }
1510: return buf.toString();
1511: } else {
1512: return getText(selectionStart, selectionEnd
1513: - selectionStart);
1514: }
1515:
1516: }
1517:
1518: /**
1519: * Replaces the selection with the specified text.
1520: * @param selectedText The replacement text for the selection
1521: */
1522: public void setSelectedText(String selectedText) {
1523: if (!editable)
1524: return;
1525:
1526: try {
1527: selectedText = fixLinefeed(selectedText);
1528: document.beginCompoundEdit();
1529:
1530: if (rectSelect) {
1531: Element map = document.getDefaultRootElement();
1532:
1533: int start = selectionStart
1534: - map.getElement(selectionStartLine)
1535: .getStartOffset();
1536: int end = selectionEnd
1537: - map.getElement(selectionEndLine)
1538: .getStartOffset();
1539:
1540: // Certain rectangles satisfy this condition...
1541: if (end < start) {
1542: int tmp = end;
1543: end = start;
1544: start = tmp;
1545: }
1546:
1547: int lastNewline = 0;
1548: int currNewline = 0;
1549:
1550: for (int i = selectionStartLine; i <= selectionEndLine; i++) {
1551: Element lineElement = map.getElement(i);
1552: int lineStart = lineElement.getStartOffset();
1553: int lineEnd = lineElement.getEndOffset() - 1;
1554: int rectStart = Math
1555: .min(lineEnd, lineStart + start);
1556:
1557: document.remove(rectStart, Math.min(lineEnd
1558: - rectStart, end - start));
1559:
1560: if (selectedText == null)
1561: continue;
1562:
1563: currNewline = selectedText.indexOf("\n",
1564: lastNewline);
1565: if (currNewline == -1) {
1566: currNewline = selectedText.length();
1567: }
1568: document.insertString(rectStart, selectedText
1569: .substring(lastNewline, currNewline), null);
1570:
1571: lastNewline = Math.min(selectedText.length(),
1572: currNewline + 1);
1573: }
1574:
1575: if (selectedText != null
1576: && currNewline != selectedText.length()) {
1577: int offset = map.getElement(selectionEndLine)
1578: .getEndOffset() - 1;
1579: document.insertString(offset, "\n", null);
1580: document.insertString(offset + 1, selectedText
1581: .substring(currNewline + 1), null);
1582: }
1583: } else {
1584: document.remove(selectionStart, selectionEnd
1585: - selectionStart);
1586:
1587: if (selectedText != null) {
1588: document.insertString(selectionStart, selectedText,
1589: null);
1590: }
1591: if (this .autoIndent) {
1592: int c = this .getCaretLine();
1593: if (c > 0 && selectedText.equals("\n")) {
1594: String s = this .getLineText(c - 1);
1595: String p = StringUtil.getStartingWhiteSpace(s);
1596: if (p != null && p.length() > 0) {
1597: document
1598: .insertString(selectionEnd, p, null);
1599: }
1600: }
1601: }
1602: }
1603: } catch (BadLocationException bl) {
1604: LogMgr.logError("JEditTextArea.setSelectedText()",
1605: "Error setting text", bl);
1606: throw new InternalError("Cannot replace selection");
1607: } finally {
1608: document.endCompoundEdit();
1609: }
1610:
1611: updateScrollBars();
1612: setCaretPosition(selectionEnd);
1613: // this.invalidate();
1614: this .repaint();
1615: }
1616:
1617: public void insertText(String text) {
1618: insertText(getCaretPosition(), text);
1619: }
1620:
1621: public void insertText(int position, String text) {
1622: try {
1623: document.beginCompoundEdit();
1624: document.insertString(position, fixLinefeed(text), null);
1625: } catch (Exception e) {
1626: LogMgr.logError("JEditTextArea.insertText()",
1627: "Error setting text", e);
1628: } finally {
1629: document.endCompoundEdit();
1630: }
1631: }
1632:
1633: public void setAutoIndent(boolean aFlag) {
1634: this .autoIndent = aFlag;
1635: }
1636:
1637: public boolean getAutoIndent() {
1638: return this .autoIndent;
1639: }
1640:
1641: /**
1642: * Returns true if this text area is editable, false otherwise.
1643: */
1644: public final boolean isEditable() {
1645: return editable;
1646: }
1647:
1648: /**
1649: * Sets if this component is editable.
1650: * @param editable True if this text area should be editable,
1651: * false otherwise
1652: */
1653: public void setEditable(boolean editable) {
1654: this .editable = editable;
1655: if (this .popup != null) {
1656: this .popup.getCutAction().setEnabled(editable);
1657: this .popup.getClearAction().setEnabled(editable);
1658: this .popup.getPasteAction().setEnabled(editable);
1659: }
1660: }
1661:
1662: /**
1663: * Returns the right click popup menu.
1664: */
1665: public final JPopupMenu getRightClickPopup() {
1666: return popup;
1667: }
1668:
1669: /**
1670: * Sets the right click popup menu.
1671: * @param popup The popup
1672: */
1673: public final void setRightClickPopup(TextPopup popup) {
1674: this .popup = popup;
1675: }
1676:
1677: /**
1678: * Returns the `magic' caret position. This can be used to preserve
1679: * the column position when moving up and down lines.
1680: */
1681: public final int getMagicCaretPosition() {
1682: return magicCaret;
1683: }
1684:
1685: /**
1686: * Sets the `magic' caret position. This can be used to preserve
1687: * the column position when moving up and down lines.
1688: * @param magicCaret The magic caret position
1689: */
1690: public final void setMagicCaretPosition(int magicCaret) {
1691: this .magicCaret = magicCaret;
1692: }
1693:
1694: /**
1695: * Similar to <code>setSelectedText()</code>, but overstrikes the
1696: * appropriate number of characters if overwrite mode is enabled.
1697: * @param str The string
1698: * @see #setSelectedText(String)
1699: * @see #isOverwriteEnabled()
1700: */
1701: public void overwriteSetSelectedText(String str) {
1702: // Don't overstrike if there is a selection
1703: if (!overwrite || selectionStart != selectionEnd) {
1704: setSelectedText(str);
1705: return;
1706: }
1707:
1708: // Don't overstrike if we're on the end of the line
1709: int caret = getCaretPosition();
1710: int caretLineEnd = getLineEndOffset(getCaretLine());
1711: if (caretLineEnd - caret <= str.length()) {
1712: setSelectedText(str);
1713: return;
1714: }
1715:
1716: document.beginCompoundEdit();
1717:
1718: try {
1719: str = fixLinefeed(str);
1720: document.remove(caret, str.length());
1721: document.insertString(caret, str, null);
1722: } catch (BadLocationException bl) {
1723: LogMgr.logError("JEditTextArea.overwriteSelectedText()",
1724: "Error setting text", bl);
1725: } finally {
1726: document.endCompoundEdit();
1727: }
1728: updateScrollBars();
1729: }
1730:
1731: /**
1732: * Returns true if overwrite mode is enabled, false otherwise.
1733: */
1734: public final boolean isOverwriteEnabled() {
1735: return overwrite;
1736: }
1737:
1738: /**
1739: * Sets if overwrite mode should be enabled.
1740: * @param overwrite True if overwrite mode should be enabled,
1741: * false otherwise.
1742: */
1743: public final void setOverwriteEnabled(boolean overwrite) {
1744: this .overwrite = overwrite;
1745: painter.invalidateSelectedLines();
1746: }
1747:
1748: /**
1749: * Returns true if the selection is rectangular, false otherwise.
1750: */
1751: public final boolean isSelectionRectangular() {
1752: return rectSelect;
1753: }
1754:
1755: /**
1756: * Sets if the selection should be rectangular.
1757: * @param rectSelect True if the selection should be rectangular,
1758: * false otherwise.
1759: */
1760: public final void setSelectionRectangular(boolean rectSelect) {
1761: this .rectSelect = rectSelect;
1762: painter.invalidateSelectedLines();
1763: }
1764:
1765: /**
1766: * Returns the position of the highlighted bracket (the bracket
1767: * matching the one before the caret)
1768: */
1769: public final int getBracketPosition() {
1770: return bracketPosition;
1771: }
1772:
1773: /**
1774: * Returns the line of the highlighted bracket (the bracket
1775: * matching the one before the caret)
1776: */
1777: public final int getBracketLine() {
1778: return bracketLine;
1779: }
1780:
1781: public final void addSelectionListener(TextSelectionListener l) {
1782: listeners.add(TextSelectionListener.class, l);
1783: }
1784:
1785: public final void removeSelectionListener(TextSelectionListener l) {
1786: listeners.remove(TextSelectionListener.class, l);
1787: }
1788:
1789: public final void addTextChangeListener(TextChangeListener l) {
1790: listeners.add(TextChangeListener.class, l);
1791: }
1792:
1793: public final void removeTextChangeListener(TextChangeListener l) {
1794: listeners.remove(TextChangeListener.class, l);
1795: }
1796:
1797: /**
1798: * Adds a caret change listener to this text area.
1799: * @param listener The listener
1800: */
1801: public final void addCaretListener(CaretListener listener) {
1802: listeners.add(CaretListener.class, listener);
1803: }
1804:
1805: /**
1806: * Removes a caret change listener from this text area.
1807: * @param listener The listener
1808: */
1809: public final void removeCaretListener(CaretListener listener) {
1810: listeners.remove(CaretListener.class, listener);
1811: }
1812:
1813: /**
1814: * Deletes the selected text from the text area and places it
1815: * into the clipboard.
1816: */
1817: public void cut() {
1818: if (editable) {
1819: copy();
1820: setSelectedText("");
1821: }
1822: }
1823:
1824: /**
1825: * Deletes the selected text from the text area
1826: **/
1827: public void clear() {
1828: if (editable) {
1829: setSelectedText("");
1830: }
1831: }
1832:
1833: /**
1834: * Places the selected text into the clipboard.
1835: */
1836: public void copy() {
1837: if (selectionStart != selectionEnd) {
1838: Clipboard clipboard = getToolkit().getSystemClipboard();
1839:
1840: String selection = getSelectedText();
1841:
1842: clipboard.setContents(new StringSelection(selection), null);
1843: }
1844: }
1845:
1846: /**
1847: * Inserts the clipboard contents into the text.
1848: */
1849: public void paste() {
1850: if (editable) {
1851: Clipboard clipboard = getToolkit().getSystemClipboard();
1852: try {
1853: String selection = ((String) clipboard
1854: .getContents(this ).getTransferData(
1855: DataFlavor.stringFlavor));
1856: setSelectedText(selection);
1857: } catch (Exception e) {
1858: getToolkit().beep();
1859: System.err
1860: .println("Clipboard does not contain a string");
1861: }
1862: }
1863: }
1864:
1865: public void setKeyEventInterceptor(KeyListener c) {
1866: this .keyEventInterceptor = c;
1867: }
1868:
1869: public void removeKeyEventInterceptor() {
1870: this .keyEventInterceptor = null;
1871: }
1872:
1873: private void forwardKeyEvent(KeyEvent evt) {
1874: switch (evt.getID()) {
1875: case KeyEvent.KEY_TYPED:
1876: keyEventInterceptor.keyTyped(evt);
1877: break;
1878: case KeyEvent.KEY_PRESSED:
1879: keyEventInterceptor.keyPressed(evt);
1880: break;
1881: case KeyEvent.KEY_RELEASED:
1882: keyEventInterceptor.keyReleased(evt);
1883: break;
1884: }
1885: }
1886:
1887: /**
1888: * Forwards key events directly to the input handler.
1889: * This is slightly faster than using a KeyListener
1890: * because some Swing overhead is avoided.
1891: */
1892: public void processKeyEvent(KeyEvent evt) {
1893: if (inputHandler == null)
1894: return;
1895: if (keyEventInterceptor != null) {
1896: forwardKeyEvent(evt);
1897: return;
1898: }
1899:
1900: int oldcount = NumberStringCache.getNumberString(
1901: this .getLineCount()).length();
1902: switch (evt.getID()) {
1903: case KeyEvent.KEY_TYPED:
1904: inputHandler.keyTyped(evt);
1905: break;
1906: case KeyEvent.KEY_PRESSED:
1907: inputHandler.keyPressed(evt);
1908: break;
1909: case KeyEvent.KEY_RELEASED:
1910: inputHandler.keyReleased(evt);
1911: break;
1912: }
1913: if (!evt.isConsumed()) {
1914: super .processKeyEvent(evt);
1915: }
1916: int newcount = NumberStringCache.getNumberString(
1917: this .getLineCount()).length();
1918: boolean changed = false;
1919:
1920: if (this .getFirstLine() < 0) {
1921: updateScrollBars();
1922: changed = true;
1923: }
1924:
1925: changed = changed || (oldcount != newcount);
1926:
1927: if (changed) {
1928: this .invalidate();
1929: this .repaint();
1930: }
1931: }
1932:
1933: protected void fireTextStatusChanged(boolean isModified) {
1934: Object[] list = listeners.getListenerList();
1935: for (int i = list.length - 2; i >= 0; i--) {
1936: if (list[i] == TextChangeListener.class) {
1937: ((TextChangeListener) list[i + 1])
1938: .textStatusChanged(isModified);
1939: }
1940: }
1941: }
1942:
1943: protected void fireSelectionEvent() {
1944: Object[] list = listeners.getListenerList();
1945: for (int i = list.length - 2; i >= 0; i--) {
1946: if (list[i] == TextSelectionListener.class) {
1947: ((TextSelectionListener) list[i + 1]).selectionChanged(
1948: this .getSelectionStart(), this
1949: .getSelectionEnd());
1950: }
1951: }
1952: }
1953:
1954: public void setStatusBar(EditorStatusbar bar) {
1955: this .statusBar = bar;
1956: updateStatusBar();
1957: }
1958:
1959: private void updateStatusBar() {
1960: if (this .statusBar != null) {
1961: int line = this .getCaretLine();
1962: this .statusBar.setEditorLocation(line + 1, this
1963: .getCaretPositionInLine(line) + 1);
1964: }
1965: }
1966:
1967: protected void fireCaretEvent() {
1968: Object[] list = listeners.getListenerList();
1969: for (int i = list.length - 2; i >= 0; i--) {
1970: if (list[i] == CaretListener.class) {
1971: ((CaretListener) list[i + 1]).caretUpdate(caretEvent);
1972: }
1973: }
1974: updateStatusBar();
1975: }
1976:
1977: protected void updateBracketHighlight(int newCaretPosition) {
1978: if (newCaretPosition == 0) {
1979: bracketPosition = bracketLine = -1;
1980: return;
1981: }
1982:
1983: try {
1984: int offset = TextUtilities.findMatchingBracket(document,
1985: newCaretPosition - 1);
1986: if (offset != -1) {
1987: bracketLine = getLineOfOffset(offset);
1988: bracketPosition = offset
1989: - getLineStartOffset(bracketLine);
1990: return;
1991: }
1992: } catch (BadLocationException bl) {
1993: LogMgr.logError("JEditTextArea.updateBracketHighlight()",
1994: "Error setting text", bl);
1995: }
1996:
1997: bracketLine = bracketPosition = -1;
1998: }
1999:
2000: protected void documentChanged(DocumentEvent evt) {
2001: DocumentEvent.ElementChange ch = evt.getChange(document
2002: .getDefaultRootElement());
2003:
2004: int count;
2005: if (ch == null) {
2006: count = 0;
2007: } else {
2008: count = ch.getChildrenAdded().length
2009: - ch.getChildrenRemoved().length;
2010: }
2011:
2012: int line = getLineOfOffset(evt.getOffset());
2013: invalidateLines(line);
2014:
2015: if (count == 0) {
2016: painter.invalidateLine(line);
2017: } else {
2018: painter.invalidateLineRange(line, (firstLine < 0 ? 0
2019: : firstLine)
2020: + visibleLines);
2021: }
2022:
2023: boolean wasModified = this .modified;
2024: this .modified = true;
2025:
2026: // only fire event if modified status is changed
2027: if (!wasModified) {
2028: this .fireTextStatusChanged(true);
2029: }
2030: updateScrollBars();
2031: }
2032:
2033: private void invalidateLines(int changedLine) {
2034: TokenMarker marker = getTokenMarker();
2035: if (marker == null)
2036: return;
2037:
2038: // In order to display multi-line literals correctly
2039: // I simply invalidate some line above and below the
2040: // currently changed line. This still can leave
2041: // incorrect tokens with regards to multiline literals
2042: // but my assumptioin is, that literals spanning more than
2043: // 'delta' number lines are used very rarely in SQL scripts.
2044:
2045: // Testing for possible literals in those lines and then only
2046: // invalidating the lines that need it, is probably
2047: // not much faster then simply invalidating a constant range of lines
2048: int startInvalid = changedLine - this .invalidationInterval;
2049: int endInvalid = changedLine + this .invalidationInterval;
2050:
2051: if (startInvalid < 0)
2052: startInvalid = 0;
2053: if (endInvalid > marker.getLineCount())
2054: endInvalid = marker.getLineCount() - 1;
2055:
2056: // re-tokenize all lines
2057: document.tokenizeLines(startInvalid, endInvalid);
2058:
2059: // re-paint the lines that need it
2060: int repaintStart = (startInvalid < getFirstLine() ? getFirstLine()
2061: : startInvalid);
2062: int repaintEnd = (endInvalid > (repaintStart + getVisibleLines()) ? repaintStart
2063: + getVisibleLines()
2064: : endInvalid);
2065: painter.invalidateLineRange(repaintStart, repaintEnd);
2066: }
2067:
2068: public boolean isModified() {
2069: return this .modified;
2070: }
2071:
2072: public void resetModified() {
2073: boolean wasModified = this .modified;
2074: this .modified = false;
2075: if (wasModified) {
2076: this .fireTextStatusChanged(false);
2077: }
2078: }
2079:
2080: /** Invoked when the mouse wheel is rotated.
2081: * @see MouseWheelEvent
2082: *
2083: */
2084: public void mouseWheelMoved(MouseWheelEvent e) {
2085: if (e.getScrollType() == MouseWheelEvent.WHEEL_UNIT_SCROLL) {
2086: int totalScrollAmount = e.getUnitsToScroll()
2087: * vertical.getUnitIncrement();
2088: vertical.setValue(vertical.getValue() + totalScrollAmount);
2089: }
2090: }
2091:
2092: class ScrollLayout implements LayoutManager {
2093: public void addLayoutComponent(String name, Component comp) {
2094: if (name.equals(CENTER))
2095: center = comp;
2096: else if (name.equals(RIGHT))
2097: right = comp;
2098: else if (name.equals(BOTTOM))
2099: bottom = comp;
2100: }
2101:
2102: public void removeLayoutComponent(Component comp) {
2103: if (center == comp)
2104: center = null;
2105: if (right == comp)
2106: right = null;
2107: if (bottom == comp)
2108: bottom = null;
2109: else
2110: leftOfScrollBar.removeElement(comp);
2111: }
2112:
2113: public Dimension preferredLayoutSize(Container parent) {
2114: Dimension dim = new Dimension();
2115: Insets insets = getInsets();
2116: dim.width = insets.left + insets.right;
2117: dim.height = insets.top + insets.bottom;
2118:
2119: Dimension centerPref = center.getPreferredSize();
2120: dim.width += centerPref.width;
2121: dim.height += centerPref.height;
2122: Dimension rightPref = right.getPreferredSize();
2123: dim.width += rightPref.width;
2124: Dimension bottomPref = bottom.getPreferredSize();
2125: dim.height += bottomPref.height;
2126:
2127: return dim;
2128: }
2129:
2130: public Dimension minimumLayoutSize(Container parent) {
2131: Dimension dim = new Dimension();
2132: Insets insets = getInsets();
2133: dim.width = insets.left + insets.right;
2134: dim.height = insets.top + insets.bottom;
2135:
2136: Dimension centerPref = center.getMinimumSize();
2137: dim.width += centerPref.width;
2138: dim.height += centerPref.height;
2139: Dimension rightPref = right.getMinimumSize();
2140: dim.width += rightPref.width;
2141: Dimension bottomPref = bottom.getMinimumSize();
2142: dim.height += bottomPref.height;
2143:
2144: return dim;
2145: }
2146:
2147: public void layoutContainer(Container parent) {
2148: Dimension size = parent.getSize();
2149: Insets insets = parent.getInsets();
2150: int itop = insets.top;
2151: int ileft = insets.left;
2152: int ibottom = insets.bottom;
2153: int iright = insets.right;
2154:
2155: int rightWidth = right.getPreferredSize().width;
2156: int bottomHeight = bottom.getPreferredSize().height;
2157: int centerWidth = size.width - rightWidth - ileft - iright;
2158: int centerHeight = size.height - bottomHeight - itop
2159: - ibottom;
2160:
2161: center.setBounds(ileft, itop, centerWidth, centerHeight);
2162:
2163: right.setBounds(ileft + centerWidth, itop, rightWidth,
2164: centerHeight);
2165:
2166: // Lay out all status components, in order
2167: Enumeration status = leftOfScrollBar.elements();
2168: while (status.hasMoreElements()) {
2169: Component comp = (Component) status.nextElement();
2170: Dimension dim = comp.getPreferredSize();
2171: comp.setBounds(ileft, itop + centerHeight, dim.width,
2172: bottomHeight);
2173: ileft += dim.width;
2174: }
2175:
2176: bottom.setBounds(ileft, itop + centerHeight, size.width
2177: - rightWidth - ileft - iright, bottomHeight);
2178: }
2179:
2180: // private members
2181: private Component center;
2182: private Component right;
2183: private Component bottom;
2184: private Vector leftOfScrollBar = new Vector();
2185: }
2186:
2187: class MutableCaretEvent extends CaretEvent {
2188: MutableCaretEvent() {
2189: super (JEditTextArea.this );
2190: }
2191:
2192: public int getDot() {
2193: return getCaretPosition();
2194: }
2195:
2196: public int getMark() {
2197: return getMarkPosition();
2198: }
2199: }
2200:
2201: class AdjustHandler implements AdjustmentListener {
2202: public void adjustmentValueChanged(final AdjustmentEvent evt) {
2203: if (!scrollBarsInitialized)
2204: return;
2205:
2206: // If this is not done, mousePressed events accumilate
2207: // and the result is that scrolling doesn't stop after
2208: // the mouse is released
2209: EventQueue.invokeLater(new Runnable() {
2210: public void run() {
2211: if (evt.getAdjustable() == vertical)
2212: setFirstLine(vertical.getValue());
2213: else
2214: setHorizontalOffset(horizontal != null ? -horizontal
2215: .getValue()
2216: : 0);
2217: }
2218: });
2219: }
2220: }
2221:
2222: class ComponentHandler extends ComponentAdapter {
2223: public void componentResized(ComponentEvent evt) {
2224: recalculateVisibleLines();
2225: scrollBarsInitialized = true;
2226: }
2227: }
2228:
2229: class DocumentHandler implements DocumentListener {
2230: public void insertUpdate(DocumentEvent evt) {
2231: documentChanged(evt);
2232:
2233: int offset = evt.getOffset();
2234: int length = evt.getLength();
2235:
2236: int newStart;
2237: int newEnd;
2238:
2239: if (selectionStart > offset
2240: || (selectionStart == selectionEnd && selectionStart == offset))
2241: newStart = selectionStart + length;
2242: else
2243: newStart = selectionStart;
2244:
2245: if (selectionEnd >= offset)
2246: newEnd = selectionEnd + length;
2247: else
2248: newEnd = selectionEnd;
2249:
2250: select(newStart, newEnd);
2251: }
2252:
2253: public void removeUpdate(DocumentEvent evt) {
2254: documentChanged(evt);
2255:
2256: int offset = evt.getOffset();
2257: int length = evt.getLength();
2258:
2259: int newStart;
2260: int newEnd;
2261:
2262: if (selectionStart > offset) {
2263: if (selectionStart > offset + length)
2264: newStart = selectionStart - length;
2265: else
2266: newStart = offset;
2267: } else
2268: newStart = selectionStart;
2269:
2270: if (selectionEnd > offset) {
2271: if (selectionEnd > offset + length)
2272: newEnd = selectionEnd - length;
2273: else
2274: newEnd = offset;
2275: } else
2276: newEnd = selectionEnd;
2277:
2278: select(newStart, newEnd);
2279: }
2280:
2281: public void changedUpdate(DocumentEvent evt) {
2282: }
2283: }
2284:
2285: class DragHandler implements MouseMotionListener {
2286: public void mouseDragged(MouseEvent evt) {
2287: if (popup != null && popup.isVisible())
2288: return;
2289:
2290: setSelectionRectangular((evt.getModifiers() & Settings
2291: .getInstance().getRectSelectionModifier()) != 0);
2292:
2293: int x = evt.getX() - painter.getGutterWidth();
2294: int y = evt.getY();
2295: select(getMarkPosition(), xyToOffset(x, y));
2296: }
2297:
2298: public void mouseMoved(MouseEvent evt) {
2299: }
2300: }
2301:
2302: class MouseHandler extends MouseAdapter {
2303: public void mousePressed(MouseEvent evt) {
2304: requestFocus();
2305:
2306: // Focus events not fired sometimes?
2307: setCaretVisible(true);
2308:
2309: int x = evt.getX() - painter.getGutterWidth();
2310: int line = yToLine(evt.getY());
2311: int offset = xToOffset(line, x);
2312: int dot = getLineStartOffset(line) + offset;
2313:
2314: if ((evt.getModifiers() & InputEvent.BUTTON3_MASK) != 0
2315: && popup != null) {
2316: if (rightClickMovesCursor && !isTextSelected()) {
2317: setCaretPosition(dot);
2318: }
2319: popup.show(painter, x, evt.getY());
2320: return;
2321: }
2322:
2323: switch (evt.getClickCount()) {
2324: case 1:
2325: doSingleClick(evt, line, offset, dot);
2326: break;
2327: case 2:
2328: // It uses the bracket matching stuff, so
2329: // it can throw a BLE
2330: try {
2331: doDoubleClick(evt, line, offset, dot);
2332: } catch (BadLocationException bl) {
2333: LogMgr.logError("MouseHandler.mousePressed()",
2334: "Error setting text", bl);
2335: }
2336: break;
2337: case 3:
2338: doTripleClick(evt, line, offset, dot);
2339: break;
2340: }
2341: }
2342:
2343: protected void doSingleClick(MouseEvent evt, int line,
2344: int offset, int dot) {
2345: if ((evt.getModifiers() & InputEvent.SHIFT_MASK) != 0) {
2346: rectSelect = (evt.getModifiers() & Settings
2347: .getInstance().getRectSelectionModifier()) != 0;
2348: select(getMarkPosition(), dot);
2349: } else {
2350: setCaretPosition(dot);
2351: }
2352: }
2353:
2354: protected void doDoubleClick(MouseEvent evt, int line,
2355: int offset, int dot) throws BadLocationException {
2356: // Ignore empty lines
2357: if (getLineLength(line) == 0)
2358: return;
2359:
2360: try {
2361: int bracket = TextUtilities.findMatchingBracket(
2362: document, Math.max(0, dot - 1));
2363: if (bracket != -1) {
2364: int mark = getMarkPosition();
2365: // Hack
2366: if (bracket > mark) {
2367: bracket++;
2368: mark--;
2369: }
2370: select(mark, bracket);
2371: return;
2372: }
2373: } catch (BadLocationException bl) {
2374: bl.printStackTrace();
2375: }
2376:
2377: // Ok, it's not a bracket... select the word
2378: String lineText = getLineText(line);
2379: char ch = lineText.charAt(Math.max(0, offset - 1));
2380:
2381: String noWordSep = Settings.getInstance()
2382: .getEditorNoWordSep();
2383: if (noWordSep == null)
2384: noWordSep = "";
2385:
2386: // If the user clicked on a non-letter char,
2387: // we select the surrounding non-letters
2388: boolean selectNoLetter = (!Character.isLetterOrDigit(ch) && noWordSep
2389: .indexOf(ch) == -1);
2390:
2391: int wordStart = 0;
2392:
2393: for (int i = offset - 1; i >= 0; i--) {
2394: ch = lineText.charAt(i);
2395: if (selectNoLetter
2396: ^ (!Character.isLetterOrDigit(ch) && noWordSep
2397: .indexOf(ch) == -1)) {
2398: wordStart = i + 1;
2399: break;
2400: }
2401: }
2402:
2403: int wordEnd = lineText.length();
2404: for (int i = offset; i < lineText.length(); i++) {
2405: ch = lineText.charAt(i);
2406: if (selectNoLetter
2407: ^ (!Character.isLetterOrDigit(ch) && noWordSep
2408: .indexOf(ch) == -1)) {
2409: wordEnd = i;
2410: break;
2411: }
2412: }
2413:
2414: int lineStart = getLineStartOffset(line);
2415: select(lineStart + wordStart, lineStart + wordEnd);
2416: }
2417:
2418: protected void doTripleClick(MouseEvent evt, int line,
2419: int offset, int dot) {
2420: select(getLineStartOffset(line), getLineEndOffset(line) - 1);
2421: }
2422: }
2423:
2424: class CaretUndo extends AbstractUndoableEdit {
2425: private int start;
2426: private int end;
2427:
2428: CaretUndo(int start, int end) {
2429: this .start = start;
2430: this .end = end;
2431: }
2432:
2433: public boolean isSignificant() {
2434: return false;
2435: }
2436:
2437: public String getPresentationName() {
2438: return "caret move";
2439: }
2440:
2441: public void undo() throws CannotUndoException {
2442: super .undo();
2443:
2444: select(start, end);
2445: }
2446:
2447: public void redo() throws CannotRedoException {
2448: super .redo();
2449:
2450: select(start, end);
2451: }
2452:
2453: public boolean addEdit(UndoableEdit edit) {
2454: if (edit instanceof CaretUndo) {
2455: CaretUndo cedit = (CaretUndo) edit;
2456: start = cedit.start;
2457: end = cedit.end;
2458: cedit.die();
2459:
2460: return true;
2461: } else
2462: return false;
2463: }
2464: }
2465:
2466: public boolean isRightClickMovesCursor() {
2467: return rightClickMovesCursor;
2468: }
2469:
2470: public void setRightClickMovesCursor(boolean rightClickMovesCursor) {
2471: this.rightClickMovesCursor = rightClickMovesCursor;
2472: }
2473: }
|