Statistics
| Revision:

svn-gvsig-desktop / trunk / org.gvsig.desktop / org.gvsig.desktop.library / org.gvsig.utils / src / main / java / org / gvsig / utils / console / jedit / JEditTextArea.java @ 40561

History | View | Annotate | Download (49.4 KB)

1
/**
2
 * gvSIG. Desktop Geographic Information System.
3
 *
4
 * Copyright (C) 2007-2013 gvSIG Association.
5
 *
6
 * This program is free software; you can redistribute it and/or
7
 * modify it under the terms of the GNU General Public License
8
 * as published by the Free Software Foundation; either version 3
9
 * of the License, or (at your option) any later version.
10
 *
11
 * This program is distributed in the hope that it will be useful,
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
14
 * GNU General Public License for more details.
15
 *
16
 * You should have received a copy of the GNU General Public License
17
 * along with this program; if not, write to the Free Software
18
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
19
 * MA  02110-1301, USA.
20
 *
21
 * For any additional information, do not hesitate to contact us
22
 * at info AT gvsig.com, or visit our website www.gvsig.com.
23
 */
24
package org.gvsig.utils.console.jedit;
25
/*
26
 * JEditTextArea.java - jEdit's text component
27
 * Copyright (C) 1999 Slava Pestov
28
 *
29
 * You may use and modify this package for any purpose. Redistribution is
30
 * permitted, in both source and binary form, provided that this notice
31
 * remains intact in all source distributions of this package.
32
 */
33

    
34
import java.awt.AWTEvent;
35
import java.awt.Component;
36
import java.awt.Container;
37
import java.awt.Dimension;
38
import java.awt.Font;
39
import java.awt.FontMetrics;
40
import java.awt.Insets;
41
import java.awt.LayoutManager;
42
import java.awt.Toolkit;
43
import java.awt.datatransfer.Clipboard;
44
import java.awt.datatransfer.DataFlavor;
45
import java.awt.datatransfer.StringSelection;
46
import java.awt.event.ActionEvent;
47
import java.awt.event.ActionListener;
48
import java.awt.event.AdjustmentEvent;
49
import java.awt.event.AdjustmentListener;
50
import java.awt.event.ComponentAdapter;
51
import java.awt.event.ComponentEvent;
52
import java.awt.event.FocusEvent;
53
import java.awt.event.FocusListener;
54
import java.awt.event.InputEvent;
55
import java.awt.event.KeyEvent;
56
import java.awt.event.MouseAdapter;
57
import java.awt.event.MouseEvent;
58
import java.awt.event.MouseMotionListener;
59
import java.util.Enumeration;
60
import java.util.Vector;
61

    
62
import javax.swing.JComponent;
63
import javax.swing.JPopupMenu;
64
import javax.swing.JScrollBar;
65
import javax.swing.SwingUtilities;
66
import javax.swing.Timer;
67
import javax.swing.event.CaretEvent;
68
import javax.swing.event.CaretListener;
69
import javax.swing.event.DocumentEvent;
70
import javax.swing.event.DocumentListener;
71
import javax.swing.event.EventListenerList;
72
import javax.swing.text.BadLocationException;
73
import javax.swing.text.Document;
74
import javax.swing.text.Element;
75
import javax.swing.text.Segment;
76
import javax.swing.text.Utilities;
77
import javax.swing.undo.AbstractUndoableEdit;
78
import javax.swing.undo.CannotRedoException;
79
import javax.swing.undo.CannotUndoException;
80
import javax.swing.undo.UndoableEdit;
81

    
82
/**
83
 * jEdit's text area component. It is more suited for editing program
84
 * source code than JEditorPane, because it drops the unnecessary features
85
 * (images, variable-width lines, and so on) and adds a whole bunch of
86
 * useful goodies such as:
87
 * <ul>
88
 * <li>More flexible key binding scheme
89
 * <li>Supports macro recorders
90
 * <li>Rectangular selection
91
 * <li>Bracket highlighting
92
 * <li>Syntax highlighting
93
 * <li>Command repetition
94
 * <li>Block caret can be enabled
95
 * </ul>
96
 * It is also faster and doesn't have as many problems. It can be used
97
 * in other applications; the only other part of jEdit it depends on is
98
 * the syntax package.<p>
99
 *
100
 * To use it in your app, treat it like any other component, for example:
101
 * <pre>JEditTextArea ta = new JEditTextArea();
102
 * ta.setTokenMarker(new JavaTokenMarker());
103
 * ta.setText("public class Test {\n"
104
 *     + "    public static void main(String[] args) {\n"
105
 *     + "        System.out.println(\"Hello World\");\n"
106
 *     + "    }\n"
107
 *     + "}");</pre>
108
 *
109
 * @author Slava Pestov
110
 * @version $Id$
111
 */
112
public class JEditTextArea extends JComponent
113
{
114
        /**
115
         * Adding components with this name to the text area will place
116
         * them left of the horizontal scroll bar. In jEdit, the status
117
         * bar is added this way.
118
         */
119
        public static String LEFT_OF_SCROLLBAR = "los";
120

    
121
        /**
122
         * Creates a new JEditTextArea with the default settings.
123
         */
124
        public JEditTextArea()
125
        {
126
                this(TextAreaDefaults.getDefaults());
127
        }
128

    
129
        /**
130
         * Creates a new JEditTextArea with the specified settings.
131
         * @param defaults The default settings
132
         */
133
        public JEditTextArea(TextAreaDefaults defaults)
134
        {
135
                // Enable the necessary events
136
                enableEvents(AWTEvent.KEY_EVENT_MASK);
137

    
138
                // Initialize some misc. stuff
139
                painter = new TextAreaPainter(this,defaults);
140
                documentHandler = new DocumentHandler();
141
                listenerList = new EventListenerList();
142
                caretEvent = new MutableCaretEvent();
143
                lineSegment = new Segment();
144
                bracketLine = bracketPosition = -1;
145
                blink = true;
146

    
147
                // Initialize the GUI
148
                setLayout(new ScrollLayout());
149
                add(CENTER,painter);
150
                add(RIGHT,vertical = new JScrollBar(JScrollBar.VERTICAL));
151
                add(BOTTOM,horizontal = new JScrollBar(JScrollBar.HORIZONTAL));
152

    
153
                // Add some event listeners
154
                vertical.addAdjustmentListener(new AdjustHandler());
155
                horizontal.addAdjustmentListener(new AdjustHandler());
156
                painter.addComponentListener(new ComponentHandler());
157
                painter.addMouseListener(new MouseHandler());
158
                painter.addMouseMotionListener(new DragHandler());
159
                addFocusListener(new FocusHandler());
160

    
161
                // Load the defaults
162
                setInputHandler(defaults.inputHandler);
163
                setDocument(defaults.document);
164
                editable = defaults.editable;
165
                caretVisible = defaults.caretVisible;
166
                caretBlinks = defaults.caretBlinks;
167
                electricScroll = defaults.electricScroll;
168

    
169
                popup = defaults.popup;
170

    
171
                // We don't seem to get the initial focus event?
172
                focusedComponent = this;
173
        }
174

    
175
        /**
176
         * Returns if this component can be traversed by pressing
177
         * the Tab key. This returns false.
178
         */
179
        public final boolean isManagingFocus()
180
        {
181
                return true;
182
        }
183

    
184
        /**
185
         * Returns the object responsible for painting this text area.
186
         */
187
        public final TextAreaPainter getPainter()
188
        {
189
                return painter;
190
        }
191

    
192
        /**
193
         * Returns the input handler.
194
         */
195
        public final InputHandler getInputHandler()
196
        {
197
                return inputHandler;
198
        }
199

    
200
        /**
201
         * Sets the input handler.
202
         * @param inputHandler The new input handler
203
         */
204
        public void setInputHandler(InputHandler inputHandler)
205
        {
206
                this.inputHandler = inputHandler;
207
        }
208

    
209
        /**
210
         * Returns true if the caret is blinking, false otherwise.
211
         */
212
        public final boolean isCaretBlinkEnabled()
213
        {
214
                return caretBlinks;
215
        }
216

    
217
        /**
218
         * Toggles caret blinking.
219
         * @param caretBlinks True if the caret should blink, false otherwise
220
         */
221
        public void setCaretBlinkEnabled(boolean caretBlinks)
222
        {
223
                this.caretBlinks = caretBlinks;
224
                if(!caretBlinks)
225
                        blink = false;
226

    
227
                painter.invalidateSelectedLines();
228
        }
229

    
230
        /**
231
         * Returns true if the caret is visible, false otherwise.
232
         */
233
        public final boolean isCaretVisible()
234
        {
235
                return (!caretBlinks || blink) && caretVisible;
236
        }
237

    
238
        /**
239
         * Sets if the caret should be visible.
240
         * @param caretVisible True if the caret should be visible, false
241
         * otherwise
242
         */
243
        public void setCaretVisible(boolean caretVisible)
244
        {
245
                this.caretVisible = caretVisible;
246
                blink = true;
247

    
248
                painter.invalidateSelectedLines();
249
        }
250

    
251
        /**
252
         * Blinks the caret.
253
         */
254
        public final void blinkCaret()
255
        {
256
                if(caretBlinks)
257
                {
258
                        blink = !blink;
259
                        painter.invalidateSelectedLines();
260
                }
261
                else
262
                        blink = true;
263
        }
264

    
265
        /**
266
         * Returns the number of lines from the top and button of the
267
         * text area that are always visible.
268
         */
269
        public final int getElectricScroll()
270
        {
271
                return electricScroll;
272
        }
273

    
274
        /**
275
         * Sets the number of lines from the top and bottom of the text
276
         * area that are always visible
277
         * @param electricScroll The number of lines always visible from
278
         * the top or bottom
279
         */
280
        public final void setElectricScroll(int electricScroll)
281
        {
282
                this.electricScroll = electricScroll;
283
        }
284

    
285
        /**
286
         * Updates the state of the scroll bars. This should be called
287
         * if the number of lines in the document changes, or when the
288
         * size of the text are changes.
289
         */
290
        public void updateScrollBars()
291
        {
292
                if(vertical != null && visibleLines != 0)
293
                {
294
                        vertical.setValues(firstLine,visibleLines,0,getLineCount());
295
                        vertical.setUnitIncrement(2);
296
                        vertical.setBlockIncrement(visibleLines);
297
                }
298

    
299
                int width = painter.getWidth();
300
                if(horizontal != null && width != 0)
301
                {
302
                        horizontal.setValues(-horizontalOffset,width,0,width * 5);
303
                        horizontal.setUnitIncrement(painter.getFontMetrics()
304
                                .charWidth('w'));
305
                        horizontal.setBlockIncrement(width / 2);
306
                }
307
        }
308

    
309
        /**
310
         * Returns the line displayed at the text area's origin.
311
         */
312
        public final int getFirstLine()
313
        {
314
                return firstLine;
315
        }
316

    
317
        /**
318
         * Sets the line displayed at the text area's origin without
319
         * updating the scroll bars.
320
         */
321
        public void setFirstLine(int firstLine)
322
        {
323
                if(firstLine == this.firstLine)
324
                        return;
325
                int oldFirstLine = this.firstLine;
326
                this.firstLine = firstLine;
327
                if(firstLine != vertical.getValue())
328
                        updateScrollBars();
329
                painter.repaint();
330
        }
331

    
332
        /**
333
         * Returns the number of lines visible in this text area.
334
         */
335
        public final int getVisibleLines()
336
        {
337
                return visibleLines;
338
        }
339

    
340
        /**
341
         * Recalculates the number of visible lines. This should not
342
         * be called directly.
343
         */
344
        public final void recalculateVisibleLines()
345
        {
346
                if(painter == null)
347
                        return;
348
                int height = painter.getHeight();
349
                int lineHeight = painter.getFontMetrics().getHeight();
350
                int oldVisibleLines = visibleLines;
351
                visibleLines = height / lineHeight;
352
                updateScrollBars();
353
        }
354

    
355
        /**
356
         * Returns the horizontal offset of drawn lines.
357
         */
358
        public final int getHorizontalOffset()
359
        {
360
                return horizontalOffset;
361
        }
362

    
363
        /**
364
         * Sets the horizontal offset of drawn lines. This can be used to
365
         * implement horizontal scrolling.
366
         * @param horizontalOffset offset The new horizontal offset
367
         */
368
        public void setHorizontalOffset(int horizontalOffset)
369
        {
370
                if(horizontalOffset == this.horizontalOffset)
371
                        return;
372
                this.horizontalOffset = horizontalOffset;
373
                if(horizontalOffset != horizontal.getValue())
374
                        updateScrollBars();
375
                painter.repaint();
376
        }
377

    
378
        /**
379
         * A fast way of changing both the first line and horizontal
380
         * offset.
381
         * @param firstLine The new first line
382
         * @param horizontalOffset The new horizontal offset
383
         * @return True if any of the values were changed, false otherwise
384
         */
385
        public boolean setOrigin(int firstLine, int horizontalOffset)
386
        {
387
                boolean changed = false;
388
                int oldFirstLine = this.firstLine;
389

    
390
                if(horizontalOffset != this.horizontalOffset)
391
                {
392
                        this.horizontalOffset = horizontalOffset;
393
                        changed = true;
394
                }
395

    
396
                if(firstLine != this.firstLine)
397
                {
398
                        this.firstLine = firstLine;
399
                        changed = true;
400
                }
401

    
402
                if(changed)
403
                {
404
                        updateScrollBars();
405
                        painter.repaint();
406
                }
407

    
408
                return changed;
409
        }
410

    
411
        /**
412
         * Ensures that the caret is visible by scrolling the text area if
413
         * necessary.
414
         * @return True if scrolling was actually performed, false if the
415
         * caret was already visible
416
         */
417
        public boolean scrollToCaret()
418
        {
419
                int line = getCaretLine();
420
                int lineStart = getLineStartOffset(line);
421
                int offset = Math.max(0,Math.min(getLineLength(line) - 1,
422
                        getCaretPosition() - lineStart));
423

    
424
                return scrollTo(line,offset);
425
        }
426

    
427
        /**
428
         * Ensures that the specified line and offset is visible by scrolling
429
         * the text area if necessary.
430
         * @param line The line to scroll to
431
         * @param offset The offset in the line to scroll to
432
         * @return True if scrolling was actually performed, false if the
433
         * line and offset was already visible
434
         */
435
        public boolean scrollTo(int line, int offset)
436
        {
437
                // visibleLines == 0 before the component is realized
438
                // we can't do any proper scrolling then, so we have
439
                // this hack...
440
                if(visibleLines == 0)
441
                {
442
                        setFirstLine(Math.max(0,line - electricScroll));
443
                        return true;
444
                }
445

    
446
                int newFirstLine = firstLine;
447
                int newHorizontalOffset = horizontalOffset;
448

    
449
                if(line < firstLine + electricScroll)
450
                {
451
                        newFirstLine = Math.max(0,line - electricScroll);
452
                }
453
                else if(line + electricScroll >= firstLine + visibleLines)
454
                {
455
                        newFirstLine = (line - visibleLines) + electricScroll + 1;
456
                        if(newFirstLine + visibleLines >= getLineCount())
457
                                newFirstLine = getLineCount() - visibleLines;
458
                        if(newFirstLine < 0)
459
                                newFirstLine = 0;
460
                }
461

    
462
                int x = _offsetToX(line,offset);
463
                int width = painter.getFontMetrics().charWidth('w');
464

    
465
                if(x < 0)
466
                {
467
                        newHorizontalOffset = Math.min(0,horizontalOffset
468
                                - x + width + 5);
469
                }
470
                else if(x + width >= painter.getWidth())
471
                {
472
                        newHorizontalOffset = horizontalOffset +
473
                                (painter.getWidth() - x) - width - 5;
474
                }
475

    
476
                return setOrigin(newFirstLine,newHorizontalOffset);
477
        }
478

    
479
        /**
480
         * Converts a line index to a y co-ordinate.
481
         * @param line The line
482
         */
483
        public int lineToY(int line)
484
        {
485
                FontMetrics fm = painter.getFontMetrics();
486
                return (line - firstLine) * fm.getHeight()
487
                        - (fm.getLeading() + fm.getMaxDescent());
488
        }
489

    
490
        /**
491
         * Converts a y co-ordinate to a line index.
492
         * @param y The y co-ordinate
493
         */
494
        public int yToLine(int y)
495
        {
496
                FontMetrics fm = painter.getFontMetrics();
497
                int height = fm.getHeight();
498
                return Math.max(0,Math.min(getLineCount() - 1,
499
                        y / height + firstLine));
500
        }
501

    
502
        /**
503
         * Converts an offset in a line into an x co-ordinate. This is a
504
         * slow version that can be used any time.
505
         * @param line The line
506
         * @param offset The offset, from the start of the line
507
         */
508
        public final int offsetToX(int line, int offset)
509
        {
510
                // don't use cached tokens
511
                painter.currentLineTokens = null;
512
                return _offsetToX(line,offset);
513
        }
514

    
515
        /**
516
         * Converts an offset in a line into an x co-ordinate. This is a
517
         * fast version that should only be used if no changes were made
518
         * to the text since the last repaint.
519
         * @param line The line
520
         * @param offset The offset, from the start of the line
521
         */
522
        public int _offsetToX(int line, int offset)
523
        {
524
                TokenMarker tokenMarker = getTokenMarker();
525

    
526
                /* Use painter's cached info for speed */
527
                FontMetrics fm = painter.getFontMetrics();
528

    
529
                getLineText(line,lineSegment);
530

    
531
                int segmentOffset = lineSegment.offset;
532
                int x = horizontalOffset;
533

    
534
                /* If syntax coloring is disabled, do simple translation */
535
                if(tokenMarker == null)
536
                {
537
                        lineSegment.count = offset;
538
                        return x + Utilities.getTabbedTextWidth(lineSegment,
539
                                fm,x,painter,0);
540
                }
541
                /* If syntax coloring is enabled, we have to do this because
542
                 * tokens can vary in width */
543
                else
544
                {
545
                        Token tokens;
546
                        if(painter.currentLineIndex == line
547
                                && painter.currentLineTokens != null)
548
                                tokens = painter.currentLineTokens;
549
                        else
550
                        {
551
                                painter.currentLineIndex = line;
552
                                tokens = painter.currentLineTokens
553
                                        = tokenMarker.markTokens(lineSegment,line);
554
                        }
555

    
556
                        Toolkit toolkit = painter.getToolkit();
557
                        Font defaultFont = painter.getFont();
558
                        SyntaxStyle[] styles = painter.getStyles();
559

    
560
                        for(;;)
561
                        {
562
                                byte id = tokens.id;
563
                                if(id == Token.END)
564
                                {
565
                                        return x;
566
                                }
567

    
568
                                if(id == Token.NULL)
569
                                        fm = painter.getFontMetrics();
570
                                else
571
                                        fm = styles[id].getFontMetrics(defaultFont);
572

    
573
                                int length = tokens.length;
574

    
575
                                if(offset + segmentOffset < lineSegment.offset + length)
576
                                {
577
                                        lineSegment.count = offset - (lineSegment.offset - segmentOffset);
578
                                        return x + Utilities.getTabbedTextWidth(
579
                                                lineSegment,fm,x,painter,0);
580
                                }
581
                                else
582
                                {
583
                                        lineSegment.count = length;
584
                                        x += Utilities.getTabbedTextWidth(
585
                                                lineSegment,fm,x,painter,0);
586
                                        lineSegment.offset += length;
587
                                }
588
                                tokens = tokens.next;
589
                        }
590
                }
591
        }
592

    
593
        /**
594
         * Converts an x co-ordinate to an offset within a line.
595
         * @param line The line
596
         * @param x The x co-ordinate
597
         */
598
        public int xToOffset(int line, int x)
599
        {
600
                TokenMarker tokenMarker = getTokenMarker();
601

    
602
                /* Use painter's cached info for speed */
603
                FontMetrics fm = painter.getFontMetrics();
604

    
605
                getLineText(line,lineSegment);
606

    
607
                char[] segmentArray = lineSegment.array;
608
                int segmentOffset = lineSegment.offset;
609
                int segmentCount = lineSegment.count;
610

    
611
                int width = horizontalOffset;
612

    
613
                if(tokenMarker == null)
614
                {
615
                        for(int i = 0; i < segmentCount; i++)
616
                        {
617
                                char c = segmentArray[i + segmentOffset];
618
                                int charWidth;
619
                                if(c == '\t')
620
                                        charWidth = (int)painter.nextTabStop(width,i)
621
                                                - width;
622
                                else
623
                                        charWidth = fm.charWidth(c);
624

    
625
                                if(painter.isBlockCaretEnabled())
626
                                {
627
                                        if(x - charWidth <= width)
628
                                                return i;
629
                                }
630
                                else
631
                                {
632
                                        if(x - charWidth / 2 <= width)
633
                                                return i;
634
                                }
635

    
636
                                width += charWidth;
637
                        }
638

    
639
                        return segmentCount;
640
                }
641
                else
642
                {
643
                        Token tokens;
644
                        if(painter.currentLineIndex == line && painter
645
                                .currentLineTokens != null)
646
                                tokens = painter.currentLineTokens;
647
                        else
648
                        {
649
                                painter.currentLineIndex = line;
650
                                tokens = painter.currentLineTokens
651
                                        = tokenMarker.markTokens(lineSegment,line);
652
                        }
653

    
654
                        int offset = 0;
655
                        Toolkit toolkit = painter.getToolkit();
656
                        Font defaultFont = painter.getFont();
657
                        SyntaxStyle[] styles = painter.getStyles();
658

    
659
                        for(;;)
660
                        {
661
                                byte id = tokens.id;
662
                                if(id == Token.END)
663
                                        return offset;
664

    
665
                                if(id == Token.NULL)
666
                                        fm = painter.getFontMetrics();
667
                                else
668
                                        fm = styles[id].getFontMetrics(defaultFont);
669

    
670
                                int length = tokens.length;
671

    
672
                                for(int i = 0; i < length; i++)
673
                                {
674
                                        char c = segmentArray[segmentOffset + offset + i];
675
                                        int charWidth;
676
                                        if(c == '\t')
677
                                                charWidth = (int)painter.nextTabStop(width,offset + i)
678
                                                        - width;
679
                                        else
680
                                                charWidth = fm.charWidth(c);
681

    
682
                                        if(painter.isBlockCaretEnabled())
683
                                        {
684
                                                if(x - charWidth <= width)
685
                                                        return offset + i;
686
                                        }
687
                                        else
688
                                        {
689
                                                if(x - charWidth / 2 <= width)
690
                                                        return offset + i;
691
                                        }
692

    
693
                                        width += charWidth;
694
                                }
695

    
696
                                offset += length;
697
                                tokens = tokens.next;
698
                        }
699
                }
700
        }
701

    
702
        /**
703
         * Converts a point to an offset, from the start of the text.
704
         * @param x The x co-ordinate of the point
705
         * @param y The y co-ordinate of the point
706
         */
707
        public int xyToOffset(int x, int y)
708
        {
709
                int line = yToLine(y);
710
                int start = getLineStartOffset(line);
711
                return start + xToOffset(line,x);
712
        }
713

    
714
        /**
715
         * Returns the document this text area is editing.
716
         */
717
        public final Document getDocument()
718
        {
719
                return document;
720
        }
721

    
722
        /**
723
         * Sets the document this text area is editing.
724
         * @param document The document
725
         */
726
        public void setDocument(SyntaxDocument document)
727
        {
728
                if(this.document == document)
729
                        return;
730
                if(this.document != null)
731
                        this.document.removeDocumentListener(documentHandler);
732
                this.document = document;
733

    
734
                document.addDocumentListener(documentHandler);
735

    
736
                select(0,0);
737
                updateScrollBars();
738
                painter.repaint();
739
        }
740

    
741
        /**
742
         * Returns the document's token marker. Equivalent to calling
743
         * <code>getDocument().getTokenMarker()</code>.
744
         */
745
        public final TokenMarker getTokenMarker()
746
        {
747
                return document.getTokenMarker();
748
        }
749

    
750
        /**
751
         * Sets the document's token marker. Equivalent to caling
752
         * <code>getDocument().setTokenMarker()</code>.
753
         * @param tokenMarker The token marker
754
         */
755
        public final void setTokenMarker(TokenMarker tokenMarker)
756
        {
757
                document.setTokenMarker(tokenMarker);
758
        }
759

    
760
        /**
761
         * Returns the length of the document. Equivalent to calling
762
         * <code>getDocument().getLength()</code>.
763
         */
764
        public final int getDocumentLength()
765
        {
766
                return document.getLength();
767
        }
768

    
769
        /**
770
         * Returns the number of lines in the document.
771
         */
772
        public final int getLineCount()
773
        {
774
                return document.getDefaultRootElement().getElementCount();
775
        }
776

    
777
        /**
778
         * Returns the line containing the specified offset.
779
         * @param offset The offset
780
         */
781
        public final int getLineOfOffset(int offset)
782
        {
783
                return document.getDefaultRootElement().getElementIndex(offset);
784
        }
785

    
786
        /**
787
         * Returns the start offset of the specified line.
788
         * @param line The line
789
         * @return The start offset of the specified line, or -1 if the line is
790
         * invalid
791
         */
792
        public int getLineStartOffset(int line)
793
        {
794
                Element lineElement = document.getDefaultRootElement()
795
                        .getElement(line);
796
                if(lineElement == null)
797
                        return -1;
798
                else
799
                        return lineElement.getStartOffset();
800
        }
801

    
802
        /**
803
         * Returns the end offset of the specified line.
804
         * @param line The line
805
         * @return The end offset of the specified line, or -1 if the line is
806
         * invalid.
807
         */
808
        public int getLineEndOffset(int line)
809
        {
810
                Element lineElement = document.getDefaultRootElement()
811
                        .getElement(line);
812
                if(lineElement == null)
813
                        return -1;
814
                else
815
                        return lineElement.getEndOffset();
816
        }
817

    
818
        /**
819
         * Returns the length of the specified line.
820
         * @param line The line
821
         */
822
        public int getLineLength(int line)
823
        {
824
                Element lineElement = document.getDefaultRootElement()
825
                        .getElement(line);
826
                if(lineElement == null)
827
                        return -1;
828
                else
829
                        return lineElement.getEndOffset()
830
                                - lineElement.getStartOffset() - 1;
831
        }
832

    
833
        /**
834
         * Returns the entire text of this text area.
835
         */
836
        public String getText()
837
        {
838
                try
839
                {
840
                        return document.getText(0,document.getLength());
841
                }
842
                catch(BadLocationException bl)
843
                {
844
                        bl.printStackTrace();
845
                        return null;
846
                }
847
        }
848

    
849
        /**
850
         * Sets the entire text of this text area.
851
         */
852
        public void setText(String text)
853
        {
854
                try
855
                {
856
                        document.beginCompoundEdit();
857
                        document.remove(0,document.getLength());
858
                        document.insertString(0,text,null);
859
                }
860
                catch(BadLocationException bl)
861
                {
862
                        bl.printStackTrace();
863
                }
864
                finally
865
                {
866
                        document.endCompoundEdit();
867
                }
868
        }
869

    
870
        /**
871
         * Returns the specified substring of the document.
872
         * @param start The start offset
873
         * @param len The length of the substring
874
         * @return The substring, or null if the offsets are invalid
875
         */
876
        public final String getText(int start, int len)
877
        {
878
                try
879
                {
880
                        return document.getText(start,len);
881
                }
882
                catch(BadLocationException bl)
883
                {
884
                        bl.printStackTrace();
885
                        return null;
886
                }
887
        }
888

    
889
        /**
890
         * Copies the specified substring of the document into a segment.
891
         * If the offsets are invalid, the segment will contain a null string.
892
         * @param start The start offset
893
         * @param len The length of the substring
894
         * @param segment The segment
895
         */
896
        public final void getText(int start, int len, Segment segment)
897
        {
898
                try
899
                {
900
                        document.getText(start,len,segment);
901
                }
902
                catch(BadLocationException bl)
903
                {
904
                        bl.printStackTrace();
905
                        segment.offset = segment.count = 0;
906
                }
907
        }
908

    
909
        /**
910
         * Returns the text on the specified line.
911
         * @param lineIndex The line
912
         * @return The text, or null if the line is invalid
913
         */
914
        public final String getLineText(int lineIndex)
915
        {
916
                int start = getLineStartOffset(lineIndex);
917
                return getText(start,getLineEndOffset(lineIndex) - start - 1);
918
        }
919

    
920
        /**
921
         * Copies the text on the specified line into a segment. If the line
922
         * is invalid, the segment will contain a null string.
923
         * @param lineIndex The line
924
         */
925
        public final void getLineText(int lineIndex, Segment segment)
926
        {
927
                int start = getLineStartOffset(lineIndex);
928
                getText(start,getLineEndOffset(lineIndex) - start - 1,segment);
929
        }
930

    
931
        /**
932
         * Returns the selection start offset.
933
         */
934
        public final int getSelectionStart()
935
        {
936
                return selectionStart;
937
        }
938

    
939
        /**
940
         * Returns the offset where the selection starts on the specified
941
         * line.
942
         */
943
        public int getSelectionStart(int line)
944
        {
945
                if(line == selectionStartLine)
946
                        return selectionStart;
947
                else if(rectSelect)
948
                {
949
                        Element map = document.getDefaultRootElement();
950
                        int start = selectionStart - map.getElement(selectionStartLine)
951
                                .getStartOffset();
952

    
953
                        Element lineElement = map.getElement(line);
954
                        int lineStart = lineElement.getStartOffset();
955
                        int lineEnd = lineElement.getEndOffset() - 1;
956
                        return Math.min(lineEnd,lineStart + start);
957
                }
958
                else
959
                        return getLineStartOffset(line);
960
        }
961

    
962
        /**
963
         * Returns the selection start line.
964
         */
965
        public final int getSelectionStartLine()
966
        {
967
                return selectionStartLine;
968
        }
969

    
970
        /**
971
         * Sets the selection start. The new selection will be the new
972
         * selection start and the old selection end.
973
         * @param selectionStart The selection start
974
         * @see #select(int,int)
975
         */
976
        public final void setSelectionStart(int selectionStart)
977
        {
978
                select(selectionStart,selectionEnd);
979
        }
980

    
981
        /**
982
         * Returns the selection end offset.
983
         */
984
        public final int getSelectionEnd()
985
        {
986
                return selectionEnd;
987
        }
988

    
989
        /**
990
         * Returns the offset where the selection ends on the specified
991
         * line.
992
         */
993
        public int getSelectionEnd(int line)
994
        {
995
                if(line == selectionEndLine)
996
                        return selectionEnd;
997
                else if(rectSelect)
998
                {
999
                        Element map = document.getDefaultRootElement();
1000
                        int end = selectionEnd - map.getElement(selectionEndLine)
1001
                                .getStartOffset();
1002

    
1003
                        Element lineElement = map.getElement(line);
1004
                        int lineStart = lineElement.getStartOffset();
1005
                        int lineEnd = lineElement.getEndOffset() - 1;
1006
                        return Math.min(lineEnd,lineStart + end);
1007
                }
1008
                else
1009
                        return getLineEndOffset(line) - 1;
1010
        }
1011

    
1012
        /**
1013
         * Returns the selection end line.
1014
         */
1015
        public final int getSelectionEndLine()
1016
        {
1017
                return selectionEndLine;
1018
        }
1019

    
1020
        /**
1021
         * Sets the selection end. The new selection will be the old
1022
         * selection start and the bew selection end.
1023
         * @param selectionEnd The selection end
1024
         * @see #select(int,int)
1025
         */
1026
        public final void setSelectionEnd(int selectionEnd)
1027
        {
1028
                select(selectionStart,selectionEnd);
1029
        }
1030

    
1031
        /**
1032
         * Returns the caret position. This will either be the selection
1033
         * start or the selection end, depending on which direction the
1034
         * selection was made in.
1035
         */
1036
        public final int getCaretPosition()
1037
        {
1038
                return (biasLeft ? selectionStart : selectionEnd);
1039
        }
1040

    
1041
        /**
1042
         * Returns the caret line.
1043
         */
1044
        public final int getCaretLine()
1045
        {
1046
                return (biasLeft ? selectionStartLine : selectionEndLine);
1047
        }
1048

    
1049
        /**
1050
         * Returns the mark position. This will be the opposite selection
1051
         * bound to the caret position.
1052
         * @see #getCaretPosition()
1053
         */
1054
        public final int getMarkPosition()
1055
        {
1056
                return (biasLeft ? selectionEnd : selectionStart);
1057
        }
1058

    
1059
        /**
1060
         * Returns the mark line.
1061
         */
1062
        public final int getMarkLine()
1063
        {
1064
                return (biasLeft ? selectionEndLine : selectionStartLine);
1065
        }
1066

    
1067
        /**
1068
         * Sets the caret position. The new selection will consist of the
1069
         * caret position only (hence no text will be selected)
1070
         * @param caret The caret position
1071
         * @see #select(int,int)
1072
         */
1073
        public final void setCaretPosition(int caret)
1074
        {
1075
                select(caret,caret);
1076
        }
1077

    
1078
        /**
1079
         * Selects all text in the document.
1080
         */
1081
        public final void selectAll()
1082
        {
1083
                select(0,getDocumentLength());
1084
        }
1085

    
1086
        /**
1087
         * Moves the mark to the caret position.
1088
         */
1089
        public final void selectNone()
1090
        {
1091
                select(getCaretPosition(),getCaretPosition());
1092
        }
1093

    
1094
        /**
1095
         * Selects from the start offset to the end offset. This is the
1096
         * general selection method used by all other selecting methods.
1097
         * The caret position will be start if start &lt; end, and end
1098
         * if end &gt; start.
1099
         * @param start The start offset
1100
         * @param end The end offset
1101
         */
1102
        public void select(int start, int end)
1103
        {
1104
                int newStart, newEnd;
1105
                boolean newBias;
1106
                if(start <= end)
1107
                {
1108
                        newStart = start;
1109
                        newEnd = end;
1110
                        newBias = false;
1111
                }
1112
                else
1113
                {
1114
                        newStart = end;
1115
                        newEnd = start;
1116
                        newBias = true;
1117
                }
1118

    
1119
                if(newStart < 0 || newEnd > getDocumentLength())
1120
                {
1121
                        throw new IllegalArgumentException("Bounds out of"
1122
                                + " range: " + newStart + "," +
1123
                                newEnd);
1124
                }
1125

    
1126
                // If the new position is the same as the old, we don't
1127
                // do all this crap, however we still do the stuff at
1128
                // the end (clearing magic position, scrolling)
1129
                if(newStart != selectionStart || newEnd != selectionEnd
1130
                        || newBias != biasLeft)
1131
                {
1132
                        int newStartLine = getLineOfOffset(newStart);
1133
                        int newEndLine = getLineOfOffset(newEnd);
1134

    
1135
                        if(painter.isBracketHighlightEnabled())
1136
                        {
1137
                                if(bracketLine != -1)
1138
                                        painter.invalidateLine(bracketLine);
1139
                                updateBracketHighlight(end);
1140
                                if(bracketLine != -1)
1141
                                        painter.invalidateLine(bracketLine);
1142
                        }
1143

    
1144
                        painter.invalidateLineRange(selectionStartLine,selectionEndLine);
1145
                        painter.invalidateLineRange(newStartLine,newEndLine);
1146

    
1147
                        document.addUndoableEdit(new CaretUndo(
1148
                                selectionStart,selectionEnd));
1149

    
1150
                        selectionStart = newStart;
1151
                        selectionEnd = newEnd;
1152
                        selectionStartLine = newStartLine;
1153
                        selectionEndLine = newEndLine;
1154
                        biasLeft = newBias;
1155

    
1156
                        fireCaretEvent();
1157
                }
1158

    
1159
                // When the user is typing, etc, we don't want the caret
1160
                // to blink
1161
                blink = true;
1162
                caretTimer.restart();
1163

    
1164
                // Disable rectangle select if selection start = selection end
1165
                if(selectionStart == selectionEnd)
1166
                        rectSelect = false;
1167

    
1168
                // Clear the `magic' caret position used by up/down
1169
                magicCaret = -1;
1170

    
1171
                scrollToCaret();
1172
        }
1173

    
1174
        /**
1175
         * Returns the selected text, or null if no selection is active.
1176
         */
1177
        public final String getSelectedText()
1178
        {
1179
                if(selectionStart == selectionEnd)
1180
                        return null;
1181

    
1182
                if(rectSelect)
1183
                {
1184
                        // Return each row of the selection on a new line
1185

    
1186
                        Element map = document.getDefaultRootElement();
1187

    
1188
                        int start = selectionStart - map.getElement(selectionStartLine)
1189
                                .getStartOffset();
1190
                        int end = selectionEnd - map.getElement(selectionEndLine)
1191
                                .getStartOffset();
1192

    
1193
                        // Certain rectangles satisfy this condition...
1194
                        if(end < start)
1195
                        {
1196
                                int tmp = end;
1197
                                end = start;
1198
                                start = tmp;
1199
                        }
1200

    
1201
                        StringBuffer buf = new StringBuffer();
1202
                        Segment seg = new Segment();
1203

    
1204
                        for(int i = selectionStartLine; i <= selectionEndLine; i++)
1205
                        {
1206
                                Element lineElement = map.getElement(i);
1207
                                int lineStart = lineElement.getStartOffset();
1208
                                int lineEnd = lineElement.getEndOffset() - 1;
1209
                                int lineLen = lineEnd - lineStart;
1210

    
1211
                                lineStart = Math.min(lineStart + start,lineEnd);
1212
                                lineLen = Math.min(end - start,lineEnd - lineStart);
1213

    
1214
                                getText(lineStart,lineLen,seg);
1215
                                buf.append(seg.array,seg.offset,seg.count);
1216

    
1217
                                if(i != selectionEndLine)
1218
                                        buf.append('\n');
1219
                        }
1220

    
1221
                        return buf.toString();
1222
                }
1223
                else
1224
                {
1225
                        return getText(selectionStart,
1226
                                selectionEnd - selectionStart);
1227
                }
1228
        }
1229

    
1230
        /**
1231
         * Replaces the selection with the specified text.
1232
         * @param selectedText The replacement text for the selection
1233
         */
1234
        public void setSelectedText(String selectedText)
1235
        {
1236
                if(!editable)
1237
                {
1238
                        throw new InternalError("Text component"
1239
                                + " read only");
1240
                }
1241

    
1242
                document.beginCompoundEdit();
1243

    
1244
                try
1245
                {
1246
                        if(rectSelect)
1247
                        {
1248
                                Element map = document.getDefaultRootElement();
1249

    
1250
                                int start = selectionStart - map.getElement(selectionStartLine)
1251
                                        .getStartOffset();
1252
                                int end = selectionEnd - map.getElement(selectionEndLine)
1253
                                        .getStartOffset();
1254

    
1255
                                // Certain rectangles satisfy this condition...
1256
                                if(end < start)
1257
                                {
1258
                                        int tmp = end;
1259
                                        end = start;
1260
                                        start = tmp;
1261
                                }
1262

    
1263
                                int lastNewline = 0;
1264
                                int currNewline = 0;
1265

    
1266
                                for(int i = selectionStartLine; i <= selectionEndLine; i++)
1267
                                {
1268
                                        Element lineElement = map.getElement(i);
1269
                                        int lineStart = lineElement.getStartOffset();
1270
                                        int lineEnd = lineElement.getEndOffset() - 1;
1271
                                        int rectStart = Math.min(lineEnd,lineStart + start);
1272

    
1273
                                        document.remove(rectStart,Math.min(lineEnd - rectStart,
1274
                                                end - start));
1275

    
1276
                                        if(selectedText == null)
1277
                                                continue;
1278

    
1279
                                        currNewline = selectedText.indexOf('\n',lastNewline);
1280
                                        if(currNewline == -1)
1281
                                                currNewline = selectedText.length();
1282

    
1283
                                        document.insertString(rectStart,selectedText
1284
                                                .substring(lastNewline,currNewline),null);
1285

    
1286
                                        lastNewline = Math.min(selectedText.length(),
1287
                                                currNewline + 1);
1288
                                }
1289

    
1290
                                if(selectedText != null &&
1291
                                        currNewline != selectedText.length())
1292
                                {
1293
                                        int offset = map.getElement(selectionEndLine)
1294
                                                .getEndOffset() - 1;
1295
                                        document.insertString(offset,"\n",null);
1296
                                        document.insertString(offset + 1,selectedText
1297
                                                .substring(currNewline + 1),null);
1298
                                }
1299
                        }
1300
                        else
1301
                        {
1302
                                document.remove(selectionStart,
1303
                                        selectionEnd - selectionStart);
1304
                                if(selectedText != null)
1305
                                {
1306
                                        document.insertString(selectionStart,
1307
                                                selectedText,null);
1308
                                }
1309
                        }
1310
                }
1311
                catch(BadLocationException bl)
1312
                {
1313
                        bl.printStackTrace();
1314
                        throw new InternalError("Cannot replace"
1315
                                + " selection");
1316
                }
1317
                // No matter what happends... stops us from leaving document
1318
                // in a bad state
1319
                finally
1320
                {
1321
                        document.endCompoundEdit();
1322
                }
1323

    
1324
                setCaretPosition(selectionEnd);
1325
        }
1326

    
1327
        /**
1328
         * Returns true if this text area is editable, false otherwise.
1329
         */
1330
        public final boolean isEditable()
1331
        {
1332
                return editable;
1333
        }
1334

    
1335
        /**
1336
         * Sets if this component is editable.
1337
         * @param editable True if this text area should be editable,
1338
         * false otherwise
1339
         */
1340
        public final void setEditable(boolean editable)
1341
        {
1342
                this.editable = editable;
1343
        }
1344

    
1345
        /**
1346
         * Returns the right click popup menu.
1347
         */
1348
        public final JPopupMenu getRightClickPopup()
1349
        {
1350
                return popup;
1351
        }
1352

    
1353
        /**
1354
         * Sets the right click popup menu.
1355
         * @param popup The popup
1356
         */
1357
        public final void setRightClickPopup(JPopupMenu popup)
1358
        {
1359
                this.popup = popup;
1360
        }
1361

    
1362
        /**
1363
         * Returns the `magic' caret position. This can be used to preserve
1364
         * the column position when moving up and down lines.
1365
         */
1366
        public final int getMagicCaretPosition()
1367
        {
1368
                return magicCaret;
1369
        }
1370

    
1371
        /**
1372
         * Sets the `magic' caret position. This can be used to preserve
1373
         * the column position when moving up and down lines.
1374
         * @param magicCaret The magic caret position
1375
         */
1376
        public final void setMagicCaretPosition(int magicCaret)
1377
        {
1378
                this.magicCaret = magicCaret;
1379
        }
1380

    
1381
        /**
1382
         * Similar to <code>setSelectedText()</code>, but overstrikes the
1383
         * appropriate number of characters if overwrite mode is enabled.
1384
         * @param str The string
1385
         * @see #setSelectedText(String)
1386
         * @see #isOverwriteEnabled()
1387
         */
1388
        public void overwriteSetSelectedText(String str)
1389
        {
1390
                // Don't overstrike if there is a selection
1391
                if(!overwrite || selectionStart != selectionEnd)
1392
                {
1393
                        setSelectedText(str);
1394
                        return;
1395
                }
1396

    
1397
                // Don't overstrike if we're on the end of
1398
                // the line
1399
                int caret = getCaretPosition();
1400
                int caretLineEnd = getLineEndOffset(getCaretLine());
1401
                if(caretLineEnd - caret <= str.length())
1402
                {
1403
                        setSelectedText(str);
1404
                        return;
1405
                }
1406

    
1407
                document.beginCompoundEdit();
1408

    
1409
                try
1410
                {
1411
                        document.remove(caret,str.length());
1412
                        document.insertString(caret,str,null);
1413
                }
1414
                catch(BadLocationException bl)
1415
                {
1416
                        bl.printStackTrace();
1417
                }
1418
                finally
1419
                {
1420
                        document.endCompoundEdit();
1421
                }
1422
        }
1423

    
1424
        /**
1425
         * Returns true if overwrite mode is enabled, false otherwise.
1426
         */
1427
        public final boolean isOverwriteEnabled()
1428
        {
1429
                return overwrite;
1430
        }
1431

    
1432
        /**
1433
         * Sets if overwrite mode should be enabled.
1434
         * @param overwrite True if overwrite mode should be enabled,
1435
         * false otherwise.
1436
         */
1437
        public final void setOverwriteEnabled(boolean overwrite)
1438
        {
1439
                this.overwrite = overwrite;
1440
                painter.invalidateSelectedLines();
1441
        }
1442

    
1443
        /**
1444
         * Returns true if the selection is rectangular, false otherwise.
1445
         */
1446
        public final boolean isSelectionRectangular()
1447
        {
1448
                return rectSelect;
1449
        }
1450

    
1451
        /**
1452
         * Sets if the selection should be rectangular.
1453
         * @param overwrite True if the selection should be rectangular,
1454
         * false otherwise.
1455
         */
1456
        public final void setSelectionRectangular(boolean rectSelect)
1457
        {
1458
                this.rectSelect = rectSelect;
1459
                painter.invalidateSelectedLines();
1460
        }
1461

    
1462
        /**
1463
         * Returns the position of the highlighted bracket (the bracket
1464
         * matching the one before the caret)
1465
         */
1466
        public final int getBracketPosition()
1467
        {
1468
                return bracketPosition;
1469
        }
1470

    
1471
        /**
1472
         * Returns the line of the highlighted bracket (the bracket
1473
         * matching the one before the caret)
1474
         */
1475
        public final int getBracketLine()
1476
        {
1477
                return bracketLine;
1478
        }
1479

    
1480
        /**
1481
         * Adds a caret change listener to this text area.
1482
         * @param listener The listener
1483
         */
1484
        public final void addCaretListener(CaretListener listener)
1485
        {
1486
                listenerList.add(CaretListener.class,listener);
1487
        }
1488

    
1489
        /**
1490
         * Removes a caret change listener from this text area.
1491
         * @param listener The listener
1492
         */
1493
        public final void removeCaretListener(CaretListener listener)
1494
        {
1495
                listenerList.remove(CaretListener.class,listener);
1496
        }
1497

    
1498
        /**
1499
         * Deletes the selected text from the text area and places it
1500
         * into the clipboard.
1501
         */
1502
        public void cut()
1503
        {
1504
                if(editable)
1505
                {
1506
                        copy();
1507
                        setSelectedText("");
1508
                }
1509
        }
1510

    
1511
        /**
1512
         * Places the selected text into the clipboard.
1513
         */
1514
        public void copy()
1515
        {
1516
                if(selectionStart != selectionEnd)
1517
                {
1518
                        Clipboard clipboard = getToolkit().getSystemClipboard();
1519

    
1520
                        String selection = getSelectedText();
1521

    
1522
                        int repeatCount = inputHandler.getRepeatCount();
1523
                        StringBuffer buf = new StringBuffer();
1524
                        for(int i = 0; i < repeatCount; i++)
1525
                                buf.append(selection);
1526

    
1527
                        clipboard.setContents(new StringSelection(buf.toString()),null);
1528
                }
1529
        }
1530

    
1531
        /**
1532
         * Inserts the clipboard contents into the text.
1533
         */
1534
        public void paste()
1535
        {
1536
                if(editable)
1537
                {
1538
                        Clipboard clipboard = getToolkit().getSystemClipboard();
1539
                        try
1540
                        {
1541
                                // The MacOS MRJ doesn't convert \r to \n,
1542
                                // so do it here
1543
                                String selection = ((String)clipboard
1544
                                        .getContents(this).getTransferData(
1545
                                        DataFlavor.stringFlavor))
1546
                                        .replace('\r','\n');
1547

    
1548
                                int repeatCount = inputHandler.getRepeatCount();
1549
                                StringBuffer buf = new StringBuffer();
1550
                                for(int i = 0; i < repeatCount; i++)
1551
                                        buf.append(selection);
1552
                                selection = buf.toString();
1553
                                setSelectedText(selection);
1554
                        }
1555
                        catch(Exception e)
1556
                        {
1557
                                getToolkit().beep();
1558
                                System.err.println("Clipboard does not"
1559
                                        + " contain a string");
1560
                        }
1561
                }
1562
        }
1563

    
1564
        /**
1565
         * Called by the AWT when this component is removed from it's parent.
1566
         * This stops clears the currently focused component.
1567
         */
1568
        public void removeNotify()
1569
        {
1570
                super.removeNotify();
1571
                if(focusedComponent == this)
1572
                        focusedComponent = null;
1573
        }
1574

    
1575
        /**
1576
         * Forwards key events directly to the input handler.
1577
         * This is slightly faster than using a KeyListener
1578
         * because some Swing overhead is avoided.
1579
         */
1580
        public void processKeyEvent(KeyEvent evt)
1581
        {
1582
                if(inputHandler == null)
1583
                        return;
1584
                switch(evt.getID())
1585
                {
1586
                case KeyEvent.KEY_TYPED:
1587
                        inputHandler.keyTyped(evt);
1588
                        break;
1589
                case KeyEvent.KEY_PRESSED:
1590
                        inputHandler.keyPressed(evt);
1591
                        break;
1592
                case KeyEvent.KEY_RELEASED:
1593
                        inputHandler.keyReleased(evt);
1594
                        break;
1595
                }
1596
        }
1597

    
1598
        // protected members
1599
        protected static String CENTER = "center";
1600
        protected static String RIGHT = "right";
1601
        protected static String BOTTOM = "bottom";
1602

    
1603
        protected static JEditTextArea focusedComponent;
1604
        protected static Timer caretTimer;
1605

    
1606
        protected TextAreaPainter painter;
1607

    
1608
        protected JPopupMenu popup;
1609

    
1610
        protected EventListenerList listenerList;
1611
        protected MutableCaretEvent caretEvent;
1612

    
1613
        protected boolean caretBlinks;
1614
        protected boolean caretVisible;
1615
        protected boolean blink;
1616

    
1617
        protected boolean editable;
1618

    
1619
        protected int firstLine;
1620
        protected int visibleLines;
1621
        protected int electricScroll;
1622

    
1623
        protected int horizontalOffset;
1624

    
1625
        protected JScrollBar vertical;
1626
        protected JScrollBar horizontal;
1627
        protected boolean scrollBarsInitialized;
1628

    
1629
        protected InputHandler inputHandler;
1630
        protected SyntaxDocument document;
1631
        protected DocumentHandler documentHandler;
1632

    
1633
        protected Segment lineSegment;
1634

    
1635
        protected int selectionStart;
1636
        protected int selectionStartLine;
1637
        protected int selectionEnd;
1638
        protected int selectionEndLine;
1639
        protected boolean biasLeft;
1640

    
1641
        protected int bracketPosition;
1642
        protected int bracketLine;
1643

    
1644
        protected int magicCaret;
1645
        protected boolean overwrite;
1646
        protected boolean rectSelect;
1647

    
1648
        protected void fireCaretEvent()
1649
        {
1650
                Object[] listeners = listenerList.getListenerList();
1651
                for(int i = listeners.length - 2; i >= 0; i--)
1652
                {
1653
                        if(listeners[i] == CaretListener.class)
1654
                        {
1655
                                ((CaretListener)listeners[i+1]).caretUpdate(caretEvent);
1656
                        }
1657
                }
1658
                super.validate();
1659
        }
1660

    
1661
        protected void updateBracketHighlight(int newCaretPosition)
1662
        {
1663
                if(newCaretPosition == 0)
1664
                {
1665
                        bracketPosition = bracketLine = -1;
1666
                        return;
1667
                }
1668

    
1669
                try
1670
                {
1671
                        int offset = TextUtilities.findMatchingBracket(
1672
                                document,newCaretPosition - 1);
1673
                        if(offset != -1)
1674
                        {
1675
                                bracketLine = getLineOfOffset(offset);
1676
                                bracketPosition = offset - getLineStartOffset(bracketLine);
1677
                                return;
1678
                        }
1679
                }
1680
                catch(BadLocationException bl)
1681
                {
1682
                        bl.printStackTrace();
1683
                }
1684

    
1685
                bracketLine = bracketPosition = -1;
1686
        }
1687

    
1688
        protected void documentChanged(DocumentEvent evt)
1689
        {
1690
                DocumentEvent.ElementChange ch = evt.getChange(
1691
                        document.getDefaultRootElement());
1692

    
1693
                int count;
1694
                if(ch == null)
1695
                        count = 0;
1696
                else
1697
                        count = ch.getChildrenAdded().length -
1698
                                ch.getChildrenRemoved().length;
1699

    
1700
                int line = getLineOfOffset(evt.getOffset());
1701
                if(count == 0)
1702
                {
1703
                        painter.invalidateLine(line);
1704
                }
1705
                // do magic stuff
1706
                else if(line < firstLine)
1707
                {
1708
                        setFirstLine(firstLine + count);
1709
                }
1710
                // end of magic stuff
1711
                else
1712
                {
1713
                        painter.invalidateLineRange(line,firstLine + visibleLines);
1714
                        updateScrollBars();
1715
                }
1716
        }
1717

    
1718
        class ScrollLayout implements LayoutManager
1719
        {
1720
                public void addLayoutComponent(String name, Component comp)
1721
                {
1722
                        if(name.equals(CENTER))
1723
                                center = comp;
1724
                        else if(name.equals(RIGHT))
1725
                                right = comp;
1726
                        else if(name.equals(BOTTOM))
1727
                                bottom = comp;
1728
                        else if(name.equals(LEFT_OF_SCROLLBAR))
1729
                                leftOfScrollBar.addElement(comp);
1730
                }
1731

    
1732
                public void removeLayoutComponent(Component comp)
1733
                {
1734
                        if(center == comp)
1735
                                center = null;
1736
                        if(right == comp)
1737
                                right = null;
1738
                        if(bottom == comp)
1739
                                bottom = null;
1740
                        else
1741
                                leftOfScrollBar.removeElement(comp);
1742
                }
1743

    
1744
                public Dimension preferredLayoutSize(Container parent)
1745
                {
1746
                        Dimension dim = new Dimension();
1747
                        Insets insets = getInsets();
1748
                        dim.width = insets.left + insets.right;
1749
                        dim.height = insets.top + insets.bottom;
1750

    
1751
                        Dimension centerPref = center.getPreferredSize();
1752
                        dim.width += centerPref.width;
1753
                        dim.height += centerPref.height;
1754
                        Dimension rightPref = right.getPreferredSize();
1755
                        dim.width += rightPref.width;
1756
                        Dimension bottomPref = bottom.getPreferredSize();
1757
                        dim.height += bottomPref.height;
1758

    
1759
                        return dim;
1760
                }
1761

    
1762
                public Dimension minimumLayoutSize(Container parent)
1763
                {
1764
                        Dimension dim = new Dimension();
1765
                        Insets insets = getInsets();
1766
                        dim.width = insets.left + insets.right;
1767
                        dim.height = insets.top + insets.bottom;
1768

    
1769
                        Dimension centerPref = center.getMinimumSize();
1770
                        dim.width += centerPref.width;
1771
                        dim.height += centerPref.height;
1772
                        Dimension rightPref = right.getMinimumSize();
1773
                        dim.width += rightPref.width;
1774
                        Dimension bottomPref = bottom.getMinimumSize();
1775
                        dim.height += bottomPref.height;
1776

    
1777
                        return dim;
1778
                }
1779

    
1780
                public void layoutContainer(Container parent)
1781
                {
1782
                        Dimension size = parent.getSize();
1783
                        Insets insets = parent.getInsets();
1784
                        int itop = insets.top;
1785
                        int ileft = insets.left;
1786
                        int ibottom = insets.bottom;
1787
                        int iright = insets.right;
1788

    
1789
                        int rightWidth = right.getPreferredSize().width;
1790
                        int bottomHeight = bottom.getPreferredSize().height;
1791
                        int centerWidth = size.width - rightWidth - ileft - iright;
1792
                        int centerHeight = size.height - bottomHeight - itop - ibottom;
1793

    
1794
                        center.setBounds(
1795
                                ileft,
1796
                                itop,
1797
                                centerWidth,
1798
                                centerHeight);
1799

    
1800
                        right.setBounds(
1801
                                ileft + centerWidth,
1802
                                itop,
1803
                                rightWidth,
1804
                                centerHeight);
1805

    
1806
                        // Lay out all status components, in order
1807
                        Enumeration status = leftOfScrollBar.elements();
1808
                        while(status.hasMoreElements())
1809
                        {
1810
                                Component comp = (Component)status.nextElement();
1811
                                Dimension dim = comp.getPreferredSize();
1812
                                comp.setBounds(ileft,
1813
                                        itop + centerHeight,
1814
                                        dim.width,
1815
                                        bottomHeight);
1816
                                ileft += dim.width;
1817
                        }
1818

    
1819
                        bottom.setBounds(
1820
                                ileft,
1821
                                itop + centerHeight,
1822
                                size.width - rightWidth - ileft - iright,
1823
                                bottomHeight);
1824
                }
1825

    
1826
                // private members
1827
                private Component center;
1828
                private Component right;
1829
                private Component bottom;
1830
                private Vector leftOfScrollBar = new Vector();
1831
        }
1832

    
1833
        static class CaretBlinker implements ActionListener
1834
        {
1835
                public void actionPerformed(ActionEvent evt)
1836
                {
1837
                        if(focusedComponent != null
1838
                                && focusedComponent.hasFocus())
1839
                                focusedComponent.blinkCaret();
1840
                }
1841
        }
1842

    
1843
        class MutableCaretEvent extends CaretEvent
1844
        {
1845
                MutableCaretEvent()
1846
                {
1847
                        super(JEditTextArea.this);
1848
                }
1849

    
1850
                public int getDot()
1851
                {
1852
                        return getCaretPosition();
1853
                }
1854

    
1855
                public int getMark()
1856
                {
1857
                        return getMarkPosition();
1858
                }
1859
        }
1860

    
1861
        class AdjustHandler implements AdjustmentListener
1862
        {
1863
                public void adjustmentValueChanged(final AdjustmentEvent evt)
1864
                {
1865
                        if(!scrollBarsInitialized)
1866
                                return;
1867

    
1868
                        // If this is not done, mousePressed events accumilate
1869
                        // and the result is that scrolling doesn't stop after
1870
                        // the mouse is released
1871
                        SwingUtilities.invokeLater(new Runnable() {
1872
                                public void run()
1873
                                {
1874
                                        if(evt.getAdjustable() == vertical)
1875
                                                setFirstLine(vertical.getValue());
1876
                                        else
1877
                                                setHorizontalOffset(-horizontal.getValue());
1878
                                }
1879
                        });
1880
                }
1881
        }
1882

    
1883
        class ComponentHandler extends ComponentAdapter
1884
        {
1885
                public void componentResized(ComponentEvent evt)
1886
                {
1887
                        recalculateVisibleLines();
1888
                        scrollBarsInitialized = true;
1889
                }
1890
        }
1891

    
1892
        class DocumentHandler implements DocumentListener
1893
        {
1894
                public void insertUpdate(DocumentEvent evt)
1895
                {
1896
                        documentChanged(evt);
1897

    
1898
                        int offset = evt.getOffset();
1899
                        int length = evt.getLength();
1900

    
1901
                        int newStart;
1902
                        int newEnd;
1903

    
1904
                        if(selectionStart > offset || (selectionStart
1905
                                == selectionEnd && selectionStart == offset))
1906
                                newStart = selectionStart + length;
1907
                        else
1908
                                newStart = selectionStart;
1909

    
1910
                        if(selectionEnd >= offset)
1911
                                newEnd = selectionEnd + length;
1912
                        else
1913
                                newEnd = selectionEnd;
1914

    
1915
                        select(newStart,newEnd);
1916
                }
1917

    
1918
                public void removeUpdate(DocumentEvent evt)
1919
                {
1920
                        documentChanged(evt);
1921

    
1922
                        int offset = evt.getOffset();
1923
                        int length = evt.getLength();
1924

    
1925
                        int newStart;
1926
                        int newEnd;
1927

    
1928
                        if(selectionStart > offset)
1929
                        {
1930
                                if(selectionStart > offset + length)
1931
                                        newStart = selectionStart - length;
1932
                                else
1933
                                        newStart = offset;
1934
                        }
1935
                        else
1936
                                newStart = selectionStart;
1937

    
1938
                        if(selectionEnd > offset)
1939
                        {
1940
                                if(selectionEnd > offset + length)
1941
                                        newEnd = selectionEnd - length;
1942
                                else
1943
                                        newEnd = offset;
1944
                        }
1945
                        else
1946
                                newEnd = selectionEnd;
1947

    
1948
                        select(newStart,newEnd);
1949
                }
1950

    
1951
                public void changedUpdate(DocumentEvent evt)
1952
                {
1953
                }
1954
        }
1955

    
1956
        class DragHandler implements MouseMotionListener
1957
        {
1958
                public void mouseDragged(MouseEvent evt)
1959
                {
1960
                        if(popup != null && popup.isVisible())
1961
                                return;
1962

    
1963
                        setSelectionRectangular((evt.getModifiers()
1964
                                & InputEvent.CTRL_MASK) != 0);
1965
                        select(getMarkPosition(),xyToOffset(evt.getX(),evt.getY()));
1966
                }
1967

    
1968
                public void mouseMoved(MouseEvent evt) {}
1969
        }
1970

    
1971
        class FocusHandler implements FocusListener
1972
        {
1973
                public void focusGained(FocusEvent evt)
1974
                {
1975
                        setCaretVisible(true);
1976
                        focusedComponent = JEditTextArea.this;
1977
                }
1978

    
1979
                public void focusLost(FocusEvent evt)
1980
                {
1981
                        setCaretVisible(false);
1982
                        focusedComponent = null;
1983
                }
1984
        }
1985

    
1986
        class MouseHandler extends MouseAdapter
1987
        {
1988
                public void mousePressed(MouseEvent evt)
1989
                {
1990
                        requestFocus();
1991

    
1992
                        // Focus events not fired sometimes?
1993
                        setCaretVisible(true);
1994
                        focusedComponent = JEditTextArea.this;
1995

    
1996
                        if((evt.getModifiers() & InputEvent.BUTTON3_MASK) != 0
1997
                                && popup != null)
1998
                        {
1999
                                popup.show(painter,evt.getX(),evt.getY());
2000
                                return;
2001
                        }
2002

    
2003
                        int line = yToLine(evt.getY());
2004
                        int offset = xToOffset(line,evt.getX());
2005
                        int dot = getLineStartOffset(line) + offset;
2006

    
2007
                        switch(evt.getClickCount())
2008
                        {
2009
                        case 1:
2010
                                doSingleClick(evt,line,offset,dot);
2011
                                break;
2012
                        case 2:
2013
                                // It uses the bracket matching stuff, so
2014
                                // it can throw a BLE
2015
                                try
2016
                                {
2017
                                        doDoubleClick(evt,line,offset,dot);
2018
                                }
2019
                                catch(BadLocationException bl)
2020
                                {
2021
                                        bl.printStackTrace();
2022
                                }
2023
                                break;
2024
                        case 3:
2025
                                doTripleClick(evt,line,offset,dot);
2026
                                break;
2027
                        }
2028
                }
2029

    
2030
                private void doSingleClick(MouseEvent evt, int line,
2031
                        int offset, int dot)
2032
                {
2033
                        if((evt.getModifiers() & InputEvent.SHIFT_MASK) != 0)
2034
                        {
2035
                                rectSelect = (evt.getModifiers() & InputEvent.CTRL_MASK) != 0;
2036
                                select(getMarkPosition(),dot);
2037
                        }
2038
                        else
2039
                                setCaretPosition(dot);
2040
                }
2041

    
2042
                private void doDoubleClick(MouseEvent evt, int line,
2043
                        int offset, int dot) throws BadLocationException
2044
                {
2045
                        // Ignore empty lines
2046
                        if(getLineLength(line) == 0)
2047
                                return;
2048

    
2049
                        try
2050
                        {
2051
                                int bracket = TextUtilities.findMatchingBracket(
2052
                                        document,Math.max(0,dot - 1));
2053
                                if(bracket != -1)
2054
                                {
2055
                                        int mark = getMarkPosition();
2056
                                        // Hack
2057
                                        if(bracket > mark)
2058
                                        {
2059
                                                bracket++;
2060
                                                mark--;
2061
                                        }
2062
                                        select(mark,bracket);
2063
                                        return;
2064
                                }
2065
                        }
2066
                        catch(BadLocationException bl)
2067
                        {
2068
                                bl.printStackTrace();
2069
                        }
2070

    
2071
                        // Ok, it's not a bracket... select the word
2072
                        String lineText = getLineText(line);
2073
                        char ch = lineText.charAt(Math.max(0,offset - 1));
2074

    
2075
                        String noWordSep = (String)document.getProperty("noWordSep");
2076
                        if(noWordSep == null)
2077
                                noWordSep = "";
2078

    
2079
                        // If the user clicked on a non-letter char,
2080
                        // we select the surrounding non-letters
2081
                        boolean selectNoLetter = (!Character
2082
                                .isLetterOrDigit(ch)
2083
                                && noWordSep.indexOf(ch) == -1);
2084

    
2085
                        int wordStart = 0;
2086

    
2087
                        for(int i = offset - 1; i >= 0; i--)
2088
                        {
2089
                                ch = lineText.charAt(i);
2090
                                if(selectNoLetter ^ (!Character
2091
                                        .isLetterOrDigit(ch) &&
2092
                                        noWordSep.indexOf(ch) == -1))
2093
                                {
2094
                                        wordStart = i + 1;
2095
                                        break;
2096
                                }
2097
                        }
2098

    
2099
                        int wordEnd = lineText.length();
2100
                        for(int i = offset; i < lineText.length(); i++)
2101
                        {
2102
                                ch = lineText.charAt(i);
2103
                                if(selectNoLetter ^ (!Character
2104
                                        .isLetterOrDigit(ch) &&
2105
                                        noWordSep.indexOf(ch) == -1))
2106
                                {
2107
                                        wordEnd = i;
2108
                                        break;
2109
                                }
2110
                        }
2111

    
2112
                        int lineStart = getLineStartOffset(line);
2113
                        select(lineStart + wordStart,lineStart + wordEnd);
2114

    
2115
                        /*
2116
                        String lineText = getLineText(line);
2117
                        String noWordSep = (String)document.getProperty("noWordSep");
2118
                        int wordStart = TextUtilities.findWordStart(lineText,offset,noWordSep);
2119
                        int wordEnd = TextUtilities.findWordEnd(lineText,offset,noWordSep);
2120

2121
                        int lineStart = getLineStartOffset(line);
2122
                        select(lineStart + wordStart,lineStart + wordEnd);
2123
                        */
2124
                }
2125

    
2126
                private void doTripleClick(MouseEvent evt, int line,
2127
                        int offset, int dot)
2128
                {
2129
                        select(getLineStartOffset(line),getLineEndOffset(line)-1);
2130
                }
2131
        }
2132

    
2133
        class CaretUndo extends AbstractUndoableEdit
2134
        {
2135
                private int start;
2136
                private int end;
2137

    
2138
                CaretUndo(int start, int end)
2139
                {
2140
                        this.start = start;
2141
                        this.end = end;
2142
                }
2143

    
2144
                public boolean isSignificant()
2145
                {
2146
                        return false;
2147
                }
2148

    
2149
                public String getPresentationName()
2150
                {
2151
                        return "caret move";
2152
                }
2153

    
2154
                public void undo() throws CannotUndoException
2155
                {
2156
                        super.undo();
2157

    
2158
                        select(start,end);
2159
                }
2160

    
2161
                public void redo() throws CannotRedoException
2162
                {
2163
                        super.redo();
2164

    
2165
                        select(start,end);
2166
                }
2167

    
2168
                public boolean addEdit(UndoableEdit edit)
2169
                {
2170
                        if(edit instanceof CaretUndo)
2171
                        {
2172
                                CaretUndo cedit = (CaretUndo)edit;
2173
                                start = cedit.start;
2174
                                end = cedit.end;
2175
                                cedit.die();
2176

    
2177
                                return true;
2178
                        }
2179
                        else
2180
                                return false;
2181
                }
2182
        }
2183

    
2184
        static
2185
        {
2186
                caretTimer = new Timer(500,new CaretBlinker());
2187
                caretTimer.setInitialDelay(500);
2188
                caretTimer.start();
2189
        }
2190
}