001: /*
002: * Gutter.java
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 1999, 2000 mike dillon
007: * Portions copyright (C) 2001, 2002 Slava Pestov
008: *
009: * This program is free software; you can redistribute it and/or
010: * modify it under the terms of the GNU General Public License
011: * as published by the Free Software Foundation; either version 2
012: * of the License, or any later version.
013: *
014: * This program is distributed in the hope that it will be useful,
015: * but WITHOUT ANY WARRANTY; without even the implied warranty of
016: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
017: * GNU General Public License for more details.
018: *
019: * You should have received a copy of the GNU General Public License
020: * along with this program; if not, write to the Free Software
021: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
022: */
023:
024: package org.gjt.sp.jedit.textarea;
025:
026: //{{{ Imports
027: import java.awt.*;
028: import java.awt.event.*;
029: import javax.swing.*;
030: import javax.swing.border.*;
031: import javax.swing.event.*;
032: import org.gjt.sp.jedit.buffer.JEditBuffer;
033: import org.gjt.sp.util.Log;
034:
035: //}}}
036:
037: /**
038: * The gutter is the component that displays folding triangles and line
039: * numbers to the left of the text area. The only methods in this class
040: * that should be called by plugins are those for adding and removing
041: * text area extensions.
042: *
043: * @see #addExtension(TextAreaExtension)
044: * @see #addExtension(int,TextAreaExtension)
045: * @see #removeExtension(TextAreaExtension)
046: * @see TextAreaExtension
047: * @see TextArea
048: *
049: * @author Mike Dillon and Slava Pestov
050: * @version $Id: Gutter.java 9861 2007-06-27 21:30:45Z kpouer $
051: */
052: public class Gutter extends JComponent implements SwingConstants {
053: //{{{ Layers
054: /**
055: * The lowest possible layer.
056: * @see #addExtension(int,TextAreaExtension)
057: * @since jEdit 4.0pre4
058: */
059: public static final int LOWEST_LAYER = Integer.MIN_VALUE;
060:
061: /**
062: * Default extension layer. This is above the wrap guide but below the
063: * bracket highlight.
064: * @since jEdit 4.0pre4
065: */
066: public static final int DEFAULT_LAYER = 0;
067:
068: /**
069: * Highest possible layer.
070: * @since jEdit 4.0pre4
071: */
072: public static final int HIGHEST_LAYER = Integer.MAX_VALUE;
073:
074: //}}}
075:
076: //{{{ Gutter constructor
077: public Gutter(TextArea textArea) {
078: this .textArea = textArea;
079:
080: setAutoscrolls(true);
081: setOpaque(true);
082: setRequestFocusEnabled(false);
083:
084: extensionMgr = new ExtensionManager();
085:
086: mouseHandler = new MouseHandler();
087: addMouseListener(mouseHandler);
088: addMouseMotionListener(mouseHandler);
089:
090: updateBorder();
091: } //}}}
092:
093: //{{{ paintComponent() method
094: public void paintComponent(Graphics _gfx) {
095: Graphics2D gfx = (Graphics2D) _gfx;
096:
097: // fill the background
098: Rectangle clip = gfx.getClipBounds();
099: gfx.setColor(getBackground());
100: gfx.fillRect(clip.x, clip.y, clip.width, clip.height);
101:
102: // if buffer is loading, don't paint anything
103: if (textArea.getBuffer().isLoading())
104: return;
105:
106: int lineHeight = textArea.getPainter().getFontMetrics()
107: .getHeight();
108:
109: if (lineHeight == 0)
110: return;
111:
112: int firstLine = clip.y / lineHeight;
113: int lastLine = (clip.y + clip.height - 1) / lineHeight;
114:
115: if (lastLine - firstLine > textArea.getVisibleLines()) {
116: Log.log(Log.ERROR, this , "BUG: firstLine=" + firstLine);
117: Log.log(Log.ERROR, this , " lastLine=" + lastLine);
118: Log.log(Log.ERROR, this , " visibleLines="
119: + textArea.getVisibleLines());
120: Log.log(Log.ERROR, this , " height=" + getHeight());
121: Log.log(Log.ERROR, this , " painter.height="
122: + textArea.getPainter().getHeight());
123: Log.log(Log.ERROR, this , " clip.y=" + clip.y);
124: Log.log(Log.ERROR, this , " clip.height=" + clip.height);
125: Log.log(Log.ERROR, this , " lineHeight=" + lineHeight);
126: }
127:
128: int y = clip.y - clip.y % lineHeight;
129:
130: extensionMgr.paintScreenLineRange(textArea, gfx, firstLine,
131: lastLine, y, lineHeight);
132:
133: for (int line = firstLine; line <= lastLine; line++, y += lineHeight) {
134: paintLine(gfx, line, y);
135: }
136: } //}}}
137:
138: //{{{ addExtension() method
139: /**
140: * Adds a text area extension, which can perform custom painting and
141: * tool tip handling.
142: * @param extension The extension
143: * @since jEdit 4.0pre4
144: */
145: public void addExtension(TextAreaExtension extension) {
146: extensionMgr.addExtension(DEFAULT_LAYER, extension);
147: repaint();
148: } //}}}
149:
150: //{{{ addExtension() method
151: /**
152: * Adds a text area extension, which can perform custom painting and
153: * tool tip handling.
154: * @param layer The layer to add the extension to. Note that more than
155: * extension can share the same layer.
156: * @param extension The extension
157: * @since jEdit 4.0pre4
158: */
159: public void addExtension(int layer, TextAreaExtension extension) {
160: extensionMgr.addExtension(layer, extension);
161: repaint();
162: } //}}}
163:
164: //{{{ removeExtension() method
165: /**
166: * Removes a text area extension. It will no longer be asked to
167: * perform custom painting and tool tip handling.
168: * @param extension The extension
169: * @since jEdit 4.0pre4
170: */
171: public void removeExtension(TextAreaExtension extension) {
172: extensionMgr.removeExtension(extension);
173: repaint();
174: } //}}}
175:
176: //{{{ getExtensions() method
177: /**
178: * Returns an array of registered text area extensions. Useful for
179: * debugging purposes.
180: * @since jEdit 4.1pre5
181: */
182: public TextAreaExtension[] getExtensions() {
183: return extensionMgr.getExtensions();
184: } //}}}
185:
186: //{{{ getToolTipText() method
187: /**
188: * Returns the tool tip to display at the specified location.
189: * @param evt The mouse event
190: */
191: public String getToolTipText(MouseEvent evt) {
192: if (textArea.getBuffer().isLoading())
193: return null;
194:
195: return extensionMgr.getToolTipText(evt.getX(), evt.getY());
196: } //}}}
197:
198: //{{{ setBorder() method
199: /**
200: * Convenience method for setting a default matte border on the right
201: * with the specified border width and color
202: * @param width The border width (in pixels)
203: * @param color1 The focused border color
204: * @param color2 The unfocused border color
205: * @param color3 The gutter/text area gap color
206: */
207: public void setBorder(int width, Color color1, Color color2,
208: Color color3) {
209: borderWidth = width;
210:
211: focusBorder = new CompoundBorder(new MatteBorder(0, 0, 0,
212: width, color3), new MatteBorder(0, 0, 0, width, color1));
213: noFocusBorder = new CompoundBorder(new MatteBorder(0, 0, 0,
214: width, color3), new MatteBorder(0, 0, 0, width, color2));
215: updateBorder();
216: } //}}}
217:
218: //{{{ updateBorder() method
219: /**
220: * Sets the border differently if the text area has focus or not.
221: */
222: public void updateBorder() {
223: if (textArea.hasFocus())
224: setBorder(focusBorder);
225: else
226: setBorder(noFocusBorder);
227: } //}}}
228:
229: //{{{ setBorder() method
230: /*
231: * JComponent.setBorder(Border) is overridden here to cache the left
232: * inset of the border (if any) to avoid having to fetch it during every
233: * repaint.
234: */
235: public void setBorder(Border border) {
236: super .setBorder(border);
237:
238: if (border == null) {
239: collapsedSize.width = 0;
240: collapsedSize.height = 0;
241: } else {
242: Insets insets = border.getBorderInsets(this );
243: collapsedSize.width = FOLD_MARKER_SIZE + insets.right;
244: collapsedSize.height = gutterSize.height = insets.top
245: + insets.bottom;
246: gutterSize.width = FOLD_MARKER_SIZE + insets.right
247: + fm.stringWidth("12345");
248: }
249:
250: revalidate();
251: } //}}}
252:
253: //{{{ setFont() method
254: /*
255: * JComponent.setFont(Font) is overridden here to cache the baseline for
256: * the font. This avoids having to get the font metrics during every
257: * repaint.
258: */
259: public void setFont(Font font) {
260: super .setFont(font);
261:
262: fm = getFontMetrics(font);
263:
264: baseline = fm.getAscent();
265:
266: Border border = getBorder();
267: if (border != null) {
268: gutterSize.width = FOLD_MARKER_SIZE
269: + border.getBorderInsets(this ).right
270: + fm.stringWidth("12345");
271: revalidate();
272: }
273: } //}}}
274:
275: //{{{ Getters and setters
276:
277: //{{{ getHighlightedForeground() method
278: /**
279: * Get the foreground color for highlighted line numbers
280: * @return The highlight color
281: */
282: public Color getHighlightedForeground() {
283: return intervalHighlight;
284: } //}}}
285:
286: //{{{ setHighlightedForeground() method
287: public void setHighlightedForeground(Color highlight) {
288: intervalHighlight = highlight;
289: } //}}}
290:
291: //{{{ getCurrentLineForeground() method
292: public Color getCurrentLineForeground() {
293: return currentLineHighlight;
294: } //}}}
295:
296: //{{{ setCurrentLineForeground() method
297: public void setCurrentLineForeground(Color highlight) {
298: currentLineHighlight = highlight;
299: } //}}}
300:
301: //{{{ getFoldColor() method
302: public Color getFoldColor() {
303: return foldColor;
304: } //}}}
305:
306: //{{{ setFoldColor() method
307: public void setFoldColor(Color foldColor) {
308: this .foldColor = foldColor;
309: } //}}}
310:
311: //{{{ getPreferredSize() method
312: /*
313: * Component.getPreferredSize() is overridden here to support the
314: * collapsing behavior.
315: */
316: public Dimension getPreferredSize() {
317: if (expanded)
318: return gutterSize;
319: else
320: return collapsedSize;
321: } //}}}
322:
323: //{{{ getMinimumSize() method
324: public Dimension getMinimumSize() {
325: return getPreferredSize();
326: } //}}}
327:
328: //{{{ getLineNumberAlignment() method
329: /**
330: * Identifies whether the horizontal alignment of the line numbers.
331: * @return Gutter.RIGHT, Gutter.CENTER, Gutter.LEFT
332: */
333: public int getLineNumberAlignment() {
334: return alignment;
335: } //}}}
336:
337: //{{{ setLineNumberAlignment() method
338: /**
339: * Sets the horizontal alignment of the line numbers.
340: * @param alignment Gutter.RIGHT, Gutter.CENTER, Gutter.LEFT
341: */
342: public void setLineNumberAlignment(int alignment) {
343: if (this .alignment == alignment)
344: return;
345:
346: this .alignment = alignment;
347:
348: repaint();
349: } //}}}
350:
351: //{{{ isExpanded() method
352: /**
353: * Identifies whether the gutter is collapsed or expanded.
354: * @return true if the gutter is expanded, false if it is collapsed
355: */
356: public boolean isExpanded() {
357: return expanded;
358: } //}}}
359:
360: //{{{ setExpanded() method
361: /**
362: * Sets whether the gutter is collapsed or expanded and force the text
363: * area to update its layout if there is a change.
364: * @param expanded true if the gutter is expanded,
365: * false if it is collapsed
366: */
367: public void setExpanded(boolean expanded) {
368: if (this .expanded == expanded)
369: return;
370:
371: this .expanded = expanded;
372:
373: textArea.revalidate();
374: } //}}}
375:
376: //{{{ toggleExpanded() method
377: /**
378: * Toggles whether the gutter is collapsed or expanded.
379: */
380: public void toggleExpanded() {
381: setExpanded(!expanded);
382: } //}}}
383:
384: //{{{ getHighlightInterval() method
385: /**
386: * Sets the number of lines between highlighted line numbers.
387: * @return The number of lines between highlighted line numbers or
388: * zero if highlighting is disabled
389: */
390: public int getHighlightInterval() {
391: return interval;
392: } //}}}
393:
394: //{{{ setHighlightInterval() method
395: /**
396: * Sets the number of lines between highlighted line numbers. Any value
397: * less than or equal to one will result in highlighting being disabled.
398: * @param interval The number of lines between highlighted line numbers
399: */
400: public void setHighlightInterval(int interval) {
401: if (interval <= 1)
402: interval = 0;
403: this .interval = interval;
404: repaint();
405: } //}}}
406:
407: //{{{ isCurrentLineHighlightEnabled() method
408: public boolean isCurrentLineHighlightEnabled() {
409: return currentLineHighlightEnabled;
410: } //}}}
411:
412: //{{{ setCurrentLineHighlightEnabled() method
413: public void setCurrentLineHighlightEnabled(boolean enabled) {
414: if (currentLineHighlightEnabled == enabled)
415: return;
416:
417: currentLineHighlightEnabled = enabled;
418:
419: repaint();
420: } //}}}
421:
422: //{{{ getStructureHighlightColor() method
423: /**
424: * Returns the structure highlight color.
425: * @since jEdit 4.2pre3
426: */
427: public final Color getStructureHighlightColor() {
428: return structureHighlightColor;
429: } //}}}
430:
431: //{{{ setStructureHighlightColor() method
432: /**
433: * Sets the structure highlight color.
434: * @param structureHighlightColor The structure highlight color
435: * @since jEdit 4.2pre3
436: */
437: public final void setStructureHighlightColor(
438: Color structureHighlightColor) {
439: this .structureHighlightColor = structureHighlightColor;
440: repaint();
441: } //}}}
442:
443: //{{{ isStructureHighlightEnabled() method
444: /**
445: * Returns true if structure highlighting is enabled, false otherwise.
446: * @since jEdit 4.2pre3
447: */
448: public final boolean isStructureHighlightEnabled() {
449: return structureHighlight;
450: } //}}}
451:
452: //{{{ setStructureHighlightEnabled() method
453: /**
454: * Enables or disables structure highlighting.
455: * @param structureHighlight True if structure highlighting should be
456: * enabled, false otherwise
457: * @since jEdit 4.2pre3
458: */
459: public final void setStructureHighlightEnabled(
460: boolean structureHighlight) {
461: this .structureHighlight = structureHighlight;
462: repaint();
463: } //}}}
464:
465: public void setMouseActionsProvider(
466: MouseActionsProvider mouseActionsProvider) {
467: mouseHandler.mouseActions = mouseActionsProvider;
468: }
469:
470: //}}}
471:
472: //{{{ Private members
473:
474: //{{{ Instance variables
475: private static final int FOLD_MARKER_SIZE = 12;
476:
477: private final TextArea textArea;
478: private MouseHandler mouseHandler;
479: private ExtensionManager extensionMgr;
480:
481: private int baseline;
482:
483: private Dimension gutterSize = new Dimension(0, 0);
484: private Dimension collapsedSize = new Dimension(0, 0);
485:
486: private Color intervalHighlight;
487: private Color currentLineHighlight;
488: private Color foldColor;
489:
490: private FontMetrics fm;
491:
492: private int alignment;
493:
494: private int interval;
495: private boolean currentLineHighlightEnabled;
496: private boolean expanded;
497:
498: private boolean structureHighlight;
499: private Color structureHighlightColor;
500:
501: private int borderWidth;
502: private Border focusBorder, noFocusBorder;
503:
504: //}}}
505:
506: //{{{ paintLine() method
507: private void paintLine(Graphics2D gfx, int line, int y) {
508: JEditBuffer buffer = textArea.getBuffer();
509: if (buffer.isLoading())
510: return;
511:
512: int lineHeight = textArea.getPainter().getFontMetrics()
513: .getHeight();
514:
515: ChunkCache.LineInfo info = textArea.chunkCache
516: .getLineInfo(line);
517: int physicalLine = info.physicalLine;
518:
519: // Skip lines beyond EOF
520: if (physicalLine == -1)
521: return;
522:
523: //{{{ Paint fold triangles
524: if (info.firstSubregion && buffer.isFoldStart(physicalLine)) {
525: int _y = y + lineHeight / 2;
526: gfx.setColor(foldColor);
527: if (textArea.displayManager.isLineVisible(physicalLine + 1)) {
528: gfx.drawLine(1, _y - 3, 10, _y - 3);
529: gfx.drawLine(2, _y - 2, 9, _y - 2);
530: gfx.drawLine(3, _y - 1, 8, _y - 1);
531: gfx.drawLine(4, _y, 7, _y);
532: gfx.drawLine(5, _y + 1, 6, _y + 1);
533: } else {
534: gfx.drawLine(4, _y - 5, 4, _y + 4);
535: gfx.drawLine(5, _y - 4, 5, _y + 3);
536: gfx.drawLine(6, _y - 3, 6, _y + 2);
537: gfx.drawLine(7, _y - 2, 7, _y + 1);
538: gfx.drawLine(8, _y - 1, 8, _y);
539: }
540: } else if (info.lastSubregion && buffer.isFoldEnd(physicalLine)) {
541: gfx.setColor(foldColor);
542: int _y = y + lineHeight / 2;
543: gfx.drawLine(4, _y, 4, _y + 3);
544: gfx.drawLine(4, _y + 3, 7, _y + 3);
545: } //}}}
546: //{{{ Paint bracket scope
547: else if (structureHighlight) {
548: StructureMatcher.Match match = textArea.getStructureMatch();
549: int caretLine = textArea.getCaretLine();
550:
551: if (textArea.isStructureHighlightVisible()
552: && physicalLine >= Math.min(caretLine,
553: match.startLine)
554: && physicalLine <= Math.max(caretLine,
555: match.startLine)) {
556: int caretScreenLine;
557: if (caretLine > textArea.getLastPhysicalLine())
558: caretScreenLine = Integer.MAX_VALUE;
559: else if (textArea.displayManager.isLineVisible(textArea
560: .getCaretLine())) {
561: caretScreenLine = textArea
562: .getScreenLineOfOffset(textArea
563: .getCaretPosition());
564: } else {
565: caretScreenLine = -1;
566: }
567:
568: int structScreenLine;
569: if (match.startLine > textArea.getLastPhysicalLine())
570: structScreenLine = Integer.MAX_VALUE;
571: else if (textArea.displayManager
572: .isLineVisible(match.startLine)) {
573: structScreenLine = textArea
574: .getScreenLineOfOffset(match.start);
575: } else {
576: structScreenLine = -1;
577: }
578:
579: if (caretScreenLine > structScreenLine) {
580: int tmp = caretScreenLine;
581: caretScreenLine = structScreenLine;
582: structScreenLine = tmp;
583: }
584:
585: gfx.setColor(structureHighlightColor);
586: if (structScreenLine == caretScreenLine) {
587: // do nothing
588: }
589: // draw |^
590: else if (line == caretScreenLine) {
591: gfx.fillRect(5, y + lineHeight / 2, 5, 2);
592: gfx.fillRect(5, y + lineHeight / 2, 2, lineHeight
593: - lineHeight / 2);
594: }
595: // draw |_
596: else if (line == structScreenLine) {
597: gfx.fillRect(5, y, 2, lineHeight / 2);
598: gfx.fillRect(5, y + lineHeight / 2, 5, 2);
599: }
600: // draw |
601: else if (line > caretScreenLine
602: && line < structScreenLine) {
603: gfx.fillRect(5, y, 2, lineHeight);
604: }
605: }
606: } //}}}
607:
608: //{{{ Paint line numbers
609: if (info.firstSubregion && expanded) {
610: String number = Integer.toString(physicalLine + 1);
611:
612: int offset;
613: switch (alignment) {
614: case RIGHT:
615: offset = gutterSize.width - collapsedSize.width
616: - (fm.stringWidth(number) + 1);
617: break;
618: case CENTER:
619: offset = ((gutterSize.width - collapsedSize.width) - fm
620: .stringWidth(number)) / 2;
621: break;
622: case LEFT:
623: default:
624: offset = 0;
625: break;
626: }
627:
628: if (physicalLine == textArea.getCaretLine()
629: && currentLineHighlightEnabled) {
630: gfx.setColor(currentLineHighlight);
631: } else if (interval > 1
632: && (physicalLine + 1) % interval == 0)
633: gfx.setColor(intervalHighlight);
634: else
635: gfx.setColor(getForeground());
636:
637: gfx.drawString(number, FOLD_MARKER_SIZE + offset, baseline
638: + y);
639: } //}}}
640: } //}}}
641:
642: //}}}
643:
644: //{{{ MouseHandler class
645: class MouseHandler extends MouseInputAdapter {
646: MouseActionsProvider mouseActions;
647: boolean drag;
648: int toolTipInitialDelay, toolTipReshowDelay;
649:
650: //{{{ mouseEntered() method
651: public void mouseEntered(MouseEvent e) {
652: ToolTipManager ttm = ToolTipManager.sharedInstance();
653: toolTipInitialDelay = ttm.getInitialDelay();
654: toolTipReshowDelay = ttm.getReshowDelay();
655: ttm.setInitialDelay(0);
656: ttm.setReshowDelay(0);
657: } //}}}
658:
659: //{{{ mouseExited() method
660: public void mouseExited(MouseEvent evt) {
661: ToolTipManager ttm = ToolTipManager.sharedInstance();
662: ttm.setInitialDelay(toolTipInitialDelay);
663: ttm.setReshowDelay(toolTipReshowDelay);
664: } //}}}
665:
666: //{{{ mousePressed() method
667: public void mousePressed(MouseEvent e) {
668: textArea.requestFocus();
669:
670: if (TextAreaMouseHandler.isPopupTrigger(e)
671: || e.getX() >= getWidth() - borderWidth * 2) {
672: e.translatePoint(-getWidth(), 0);
673: textArea.mouseHandler.mousePressed(e);
674: drag = true;
675: } else {
676: JEditBuffer buffer = textArea.getBuffer();
677:
678: int screenLine = e.getY()
679: / textArea.getPainter().getFontMetrics()
680: .getHeight();
681:
682: int line = textArea.chunkCache.getLineInfo(screenLine).physicalLine;
683:
684: if (line == -1)
685: return;
686:
687: //{{{ Determine action
688: String defaultAction;
689: String variant;
690: if (buffer.isFoldStart(line)) {
691: defaultAction = "toggle-fold";
692: variant = "fold";
693: } else if (structureHighlight
694: && textArea.isStructureHighlightVisible()
695: && textArea.lineInStructureScope(line)) {
696: defaultAction = "match-struct";
697: variant = "struct";
698: } else
699: return;
700:
701: String action = null;
702:
703: if (mouseActions != null)
704: action = mouseActions.getActionForEvent(e, variant);
705:
706: if (action == null)
707: action = defaultAction;
708: //}}}
709:
710: //{{{ Handle actions
711: StructureMatcher.Match match = textArea
712: .getStructureMatch();
713:
714: if (action.equals("select-fold")) {
715: textArea.displayManager.expandFold(line, true);
716: textArea.selectFold(line);
717: } else if (action.equals("narrow-fold")) {
718: int[] lines = buffer.getFoldAtLine(line);
719: textArea.displayManager.narrow(lines[0], lines[1]);
720: } else if (action.startsWith("toggle-fold")) {
721: if (textArea.displayManager.isLineVisible(line + 1)) {
722: textArea.collapseFold(line);
723: } else {
724: if (action.endsWith("-fully")) {
725: textArea.displayManager.expandFold(line,
726: true);
727: } else {
728: textArea.displayManager.expandFold(line,
729: false);
730: }
731: }
732: } else if (action.equals("match-struct")) {
733: if (match != null)
734: textArea.setCaretPosition(match.end);
735: } else if (action.equals("select-struct")) {
736: if (match != null) {
737: match.matcher.selectMatch(textArea);
738: }
739: } else if (action.equals("narrow-struct")) {
740: if (match != null) {
741: int start = Math.min(match.startLine, textArea
742: .getCaretLine());
743: int end = Math.max(match.endLine, textArea
744: .getCaretLine());
745: textArea.displayManager.narrow(start, end);
746: }
747: } //}}}
748: }
749: } //}}}
750:
751: //{{{ mouseDragged() method
752: public void mouseDragged(MouseEvent e) {
753: if (drag /* && e.getX() >= getWidth() - borderWidth * 2 */) {
754: e.translatePoint(-getWidth(), 0);
755: textArea.mouseHandler.mouseDragged(e);
756: }
757: } //}}}
758:
759: //{{{ mouseReleased() method
760: public void mouseReleased(MouseEvent e) {
761: if (drag && e.getX() >= getWidth() - borderWidth * 2) {
762: e.translatePoint(-getWidth(), 0);
763: textArea.mouseHandler.mouseReleased(e);
764: }
765:
766: drag = false;
767: } //}}}
768: } //}}}
769: }
|