|
1
21
22 package org.armedbear.j;
23
24 import java.awt.Color  ;
25 import java.awt.Font ;
26 import java.awt.FontMetrics ;
27 import java.awt.Graphics2D ;
28 import java.awt.Graphics ;
29 import java.awt.Image ;
30 import java.awt.Point ;
31 import java.awt.Rectangle ;
32 import java.awt.RenderingHints ;
33 import java.awt.Toolkit ;
34 import java.awt.event.ActionEvent ;
35 import java.awt.event.ActionListener ;
36 import java.awt.event.FocusEvent ;
37 import java.awt.event.FocusListener ;
38 import java.awt.event.MouseEvent ;
39 import java.awt.font.GlyphVector ;
40 import java.util.HashMap ;
41 import javax.swing.JComponent ;
42 import javax.swing.SwingUtilities ;
43 import javax.swing.Timer ;
44
45 public final class Display extends JComponent implements Constants,
46 ActionListener , FocusListener
47 {
48 private static final int MAX_LINE_NUMBER_CHARS = 6;
49
50 private static final Preferences preferences = Editor.preferences();
51
52 private static Font plainFont;
53 private static Font boldFont;
54 private static Font italicFont;
55
56 private static int charHeight;
57 private static int charDescent;
58 private static int charAscent;
59 private static int charLeading;
60 private static int charWidth;
61 private static int spaceWidth; private static int minCharWidth;
63
64 private static boolean antialias;
65 private static boolean underlineBold;
66 private static boolean emulateBold;
67
68 private static int changeMarkWidth;
69
70 private static Font gutterFont;
71 private static int gutterCharAscent;
72 private static int gutterCharWidth;
73
74 private static boolean showGutterBorder = true;
75
76 private static int leftMargin;
77
78 private final HashMap changedLines = new HashMap ();
79
80 private final Editor editor;
81
82 private Line topLine;
83 private int pixelsAboveTopLine;
84
85 int shift = 0;
87
88 int caretCol;
92
93 private char[] textArray;
94 private int[] formatArray;
95
96 private int updateFlag;
97
98 private boolean showChangeMarks;
100 private boolean enableChangeMarks;
101 private boolean showLineNumbers;
102 private int gutterWidth;
103 private Color changeColor;
104 private Color savedChangeColor;
105 private Color lineNumberColor;
106 private int verticalRuleX;
107 private Color verticalRuleColor;
108 private Color gutterBorderColor;
109 private boolean highlightBrackets;
110 private boolean highlightMatchingBracket;
111 private Position posBracket;
112 private Position posMatch;
113
114 private Timer timer;
115 private boolean caretVisible = true;
116
117 public Display(Editor editor)
118 {
119 this.editor = editor;
120 if (plainFont == null)
121 initializeStaticValues();
122 initialize();
123 setFocusTraversalKeysEnabled(false);
124 setToolTipText("");
125 }
126
127 public static void initializeStaticValues()
128 {
129 final String fontName = preferences.getStringProperty(Property.FONT_NAME);
130 final int fontSize = preferences.getIntegerProperty(Property.FONT_SIZE);
131
132 plainFont = new Font (fontName, Font.PLAIN, fontSize);
133 boldFont = new Font (fontName, Font.BOLD, fontSize);
134 if (preferences.getBooleanProperty(Property.ENABLE_ITALICS))
135 italicFont = new Font (fontName, Font.ITALIC, fontSize);
136 else
137 italicFont = plainFont;
138
139 FontMetrics fm = Toolkit.getDefaultToolkit().getFontMetrics(plainFont);
140
141 final int plainAscent = fm.getAscent();
142 final int plainDescent = fm.getDescent();
143 final int plainLeading = fm.getLeading();
144
145 charWidth = fm.charWidth('a');
146 spaceWidth = fm.charWidth(' ');
147 minCharWidth = getMinCharWidth(fm);
148
149 leftMargin = charWidth;
150
151 fm = Toolkit.getDefaultToolkit().getFontMetrics(boldFont);
152
153 final int boldAscent = fm.getAscent();
154 final int boldDescent = fm.getDescent();
155 final int boldLeading = fm.getLeading();
156
157 charAscent = plainAscent;
158 if (boldAscent > charAscent)
159 charAscent = boldAscent;
160
161 charDescent = plainDescent;
162 if (boldDescent > charDescent)
163 charDescent = boldDescent;
164
165 charLeading = (plainLeading > 0 || boldLeading > 0) ? 1 : 0;
167
168 final int adjustAscent = preferences.getIntegerProperty(Property.ADJUST_ASCENT);
170 final int adjustDescent = preferences.getIntegerProperty(Property.ADJUST_DESCENT);
171 final int adjustLeading = preferences.getIntegerProperty(Property.ADJUST_LEADING);
172
173 if (charAscent + adjustAscent >= 0)
174 charAscent += adjustAscent;
175 if (charDescent + adjustDescent >= 0)
176 charDescent += adjustDescent;
177 if (charLeading + adjustLeading >= 0)
178 charLeading += adjustLeading;
179
180 charHeight = charAscent + charDescent + charLeading;
181
182 antialias = preferences.getBooleanProperty(Property.ANTIALIAS);
183 underlineBold = preferences.getBooleanProperty(Property.UNDERLINE_BOLD);
184 emulateBold = preferences.getBooleanProperty(Property.EMULATE_BOLD);
185
186 String gutterFontName = preferences.getStringProperty(Property.GUTTER_FONT_NAME);
187 if (gutterFontName == null)
188 gutterFontName = fontName;
189 int gutterFontSize = preferences.getIntegerProperty(Property.GUTTER_FONT_SIZE);
190 if (gutterFontSize == 0)
191 gutterFontSize = fontSize;
192 gutterFont = new Font (gutterFontName, Font.PLAIN, gutterFontSize);
193
194 fm = Toolkit.getDefaultToolkit().getFontMetrics(gutterFont);
195 gutterCharAscent = fm.getAscent();
196 gutterCharWidth = fm.charWidth('0');
197
198 changeMarkWidth =
199 preferences.getIntegerProperty(Property.CHANGE_MARK_WIDTH);
200 }
201
202 public synchronized void initialize()
203 {
204 paintLineImage = null;
206
207 int size = Toolkit.getDefaultToolkit().getScreenSize().width * 5 / (minCharWidth * 4);
211 textArray = new char[size];
212 formatArray = new int[size];
213
214 if (preferences.getBooleanProperty(Property.BLINK_CARET)) {
215 if (timer == null) {
216 timer = new Timer (500, this);
217 addFocusListener(this);
218 }
219 } else {
220 if (timer != null) {
221 timer.stop();
222 timer = null;
223 removeFocusListener(this);
224 setCaretVisible(true);
225 }
226 }
227 }
228
229 protected void finalize() throws Throwable
230 {
231 if (timer != null) {
232 timer.stop();
233 timer = null;
234 }
235 }
236
237 private static final int getMinCharWidth(FontMetrics fm)
238 {
239 int minWidth = Integer.MAX_VALUE;
240 int[] widths = fm.getWidths();
241 int limit = widths.length > 0x7e ? 0x7e : widths.length;
242 for (int i = limit; i >= 32; i--)
243 if (widths[i] != 0 && widths[i] < minWidth)
244 minWidth = widths[i];
245 return minWidth;
246 }
247
248 public static final int getCharHeight()
249 {
250 return charHeight;
251 }
252
253 public static final int getCharWidth()
254 {
255 return charWidth;
256 }
257
258 public static final int getImageBorderHeight()
259 {
260 return 5;
261 }
262
263 public static final int getImageBorderWidth()
264 {
265 return 5;
266 }
267
268 public final Line getTopLine()
269 {
270 return topLine;
271 }
272
273 public final int getTopLineNumber()
274 {
275 return topLine.lineNumber();
276 }
277
278 public final void setTopLine(Line line)
279 {
280 topLine = line;
281 pixelsAboveTopLine = 0;
282 }
283
284 public final int getPixelsAboveTopLine()
285 {
286 return pixelsAboveTopLine;
287 }
288
289 public final void setPixelsAboveTopLine(int pixels)
290 {
291 pixelsAboveTopLine = pixels;
292 }
293
294 public final int getShift()
295 {
296 return shift;
297 }
298
299 public final void setShift(int n)
300 {
301 this.shift = n;
302 }
303
304 public final int getCaretCol()
305 {
306 return caretCol;
307 }
308
309 public final void setCaretCol(int n)
310 {
311 caretCol = n;
312 }
313
314 public int getAbsoluteCaretCol()
315 {
316 return caretCol + shift;
317 }
318
319 public void setAbsoluteCaretCol(int col)
320 {
321 caretCol = col - shift;
322 }
323
324 public final void repaintNow()
325 {
326 paintImmediately(0, 0, getWidth(), getHeight());
327 }
328
329 public synchronized void repaintChangedLines()
330 {
331 if (!Editor.displayReady())
332 return;
333 if ((updateFlag & REPAINT) == REPAINT) {
334 repaint();
335 return;
336 }
337 if (changedLines.isEmpty())
338 return;
339 final Buffer buffer = editor.getBuffer();
340 initializePaint();
341 try {
342 buffer.lockRead();
343 }
344 catch (InterruptedException e) {
345 Log.error(e);
346 return;
347 }
348 try {
349 Graphics2D g2d = (Graphics2D ) getGraphics();
350 if (g2d != null) {
351 Line line = topLine;
352 int y = - pixelsAboveTopLine;
353 final int limit = getHeight();
354 while (line != null && y < limit) {
355 if (changedLines.containsKey(line))
356 paintLine(line, g2d, y);
357 y += line.getHeight();
358 line = line.nextVisible();
359 }
360 if (y < limit) {
361 g2d.setColor(editor.getFormatter().getBackgroundColor());
362 final int height = limit - y;
363 g2d.fillRect(0, y, getWidth(), height);
364 if (showLineNumbers)
365 drawGutterBorder(g2d, y, height);
366 drawVerticalRule(g2d, y, height);
367 }
368 drawCaret(g2d);
369 }
370 }
371 finally {
372 buffer.unlockRead();
373 }
374 changedLines.clear();
375 }
376
377 public void moveCaretToDotCol()
379 {
380 if (editor.getDot() == null)
381 return;
382 int absCol = editor.getDotCol();
383 if (caretCol != absCol - shift) {
384 caretCol = absCol - shift;
385 lineChanged(editor.getDotLine());
386 }
387 setUpdateFlag(REFRAME);
388 }
389
390 private int getY(Line line)
392 {
393 int y = - pixelsAboveTopLine;
394 int limit = getHeight();
395 for (Line l = topLine; y < limit && l != null && l != line; l = l.nextVisible())
396 y += l.getHeight();
397 return y;
398 }
399
400 private int getAbsoluteY(Line line)
402 {
403 int y = 0;
404 for (Line l = editor.getBuffer().getFirstLine(); l != null && l != line; l = l.nextVisible())
405 y += l.getHeight();
406 return y;
407 }
408
409 private void initializePaint()
410 {
411 final Buffer buffer = editor.getBuffer();
412 final Mode mode = editor.getMode();
413 showChangeMarks = buffer.getBooleanProperty(Property.SHOW_CHANGE_MARKS);
414 enableChangeMarks = showChangeMarks && !buffer.isNewFile();
415 if (showChangeMarks) {
416 changeColor = mode.getColorProperty(Property.COLOR_CHANGE);
417 if (changeColor == null)
418 changeColor = DefaultTheme.getColor("change");
419 savedChangeColor = mode.getColorProperty(Property.COLOR_SAVED_CHANGE);
420 if (savedChangeColor == null)
421 savedChangeColor = DefaultTheme.getColor("savedChange");
422 }
423 showLineNumbers = buffer.getBooleanProperty(Property.SHOW_LINE_NUMBERS);
424 gutterWidth = getGutterWidth(showChangeMarks, showLineNumbers);
425 if (showLineNumbers) {
426 lineNumberColor = mode.getColorProperty(Property.COLOR_LINE_NUMBER);
427 if (lineNumberColor == null)
428 lineNumberColor = DefaultTheme.getColor("lineNumber");
429 gutterBorderColor = mode.getColorProperty(Property.COLOR_GUTTER_BORDER);
430 if (gutterBorderColor == null)
431 gutterBorderColor = DefaultTheme.getColor("gutterBorder");
432 }
433 int col = buffer.getIntegerProperty(Property.VERTICAL_RULE);
434 if (col != 0) {
435 verticalRuleX = gutterWidth + (col - shift) * charWidth - 1;
436 verticalRuleColor = mode.getColorProperty(Property.COLOR_VERTICAL_RULE);
437 if (verticalRuleColor == null)
438 verticalRuleColor = DefaultTheme.getColor("verticalRule");
439 } else
440 verticalRuleX = 0;
441 highlightBrackets =
442 buffer.getBooleanProperty(Property.HIGHLIGHT_BRACKETS);
443 highlightMatchingBracket = highlightBrackets ||
444 buffer.getBooleanProperty(Property.HIGHLIGHT_MATCHING_BRACKET);
445
446 if (highlightMatchingBracket) {
447 Position oldPosMatch = posMatch;
448 posBracket = null;
449 posMatch = null;
450 if (editor.getDot() != null) {
451 Position dot = editor.getDotCopy();
452 char c = dot.getChar();
453 if (c == '{' || c == '[' || c == '(') {
454 posBracket = dot;
455 posMatch = editor.findMatchInternal(dot, 200);
456 } else if (dot.getOffset() > 0) {
457 int end = editor.getBuffer().getCol(dot.getLine(),
458 dot.getLine().length());
459 if (shift + caretCol <= end) {
460 dot.skip(-1);
461 c = dot.getChar();
462 if (c == '}' || c == ']' || c == ')') {
463 posBracket = dot;
464 posMatch = editor.findMatchInternal(dot, 200);
465 }
466 }
467 }
468 }
469 if (oldPosMatch != null && oldPosMatch != posMatch)
470 lineChanged(oldPosMatch.getLine());
471 if (posMatch != null && posMatch != oldPosMatch)
472 lineChanged(posMatch.getLine());
473 if (!highlightBrackets)
474 posBracket = null;
475 }
476 }
477
478 private void drawVerticalRule(Graphics g, int y, int height)
479 {
480 if (verticalRuleX > gutterWidth) {
481 g.setColor(verticalRuleColor);
482 g.drawLine(verticalRuleX, y, verticalRuleX, y + height);
483 }
484 }
485
486 private Position dragCaretPos;
487
488 public void setDragCaretPos(Position pos)
489 {
490 if (dragCaretPos != null)
491 lineChanged(dragCaretPos.getLine());
492 dragCaretPos = pos;
493 if (pos != null)
494 lineChanged(pos.getLine());
495 }
496
497 private int dragCaretCol;
498
499 public void setDragCaretCol(int col)
500 {
501 dragCaretCol = col;
502 }
503
504 private void drawDragCaret()
506 {
507 if (dragCaretPos == null)
508 return;
509 if (topLine == null)
510 return;
511 final Line line = dragCaretPos.getLine();
512 if (line.lineNumber() < topLine.lineNumber())
513 return;
514 final int absCol;
515 if (editor.getBuffer().getBooleanProperty(Property.RESTRICT_CARET))
516 absCol = editor.getBuffer().getCol(dragCaretPos);
517 else
518 absCol = dragCaretCol; if (absCol < shift)
520 return;
521 final int col = absCol - shift;
522 formatLine(line, shift, col);
523 Graphics2D g2d = (Graphics2D ) getGraphics();
524 final int x =
525 gutterWidth + measureLine(g2d, textArray, col, formatArray);
526 final int y = getY(line);
527 g2d.setColor(editor.getFormatter().getCaretColor());
528 g2d.fillRect(x, y, 1, charAscent + charDescent);
529 }
530
531 private void drawCaret(Graphics2D g2d)
533 {
534 if (dragCaretPos != null) {
535 drawDragCaret();
536 return;
537 }
538
539 if (!caretVisible)
540 return;
541 if (topLine == null)
542 return;
543 if (editor != Editor.currentEditor())
544 return;
545 if (editor.getDot() == null)
546 return;
547 if (editor.getMark() != null && !editor.getMark().equals(editor.getDot()))
548 return;
549 if (caretCol < 0)
550 return;
551 if (!editor.getFrame().isActive())
552 return;
553 if (editor.getFrame().getFocusedComponent() != this)
554 return;
555 final Line dotLine = editor.getDotLine();
556 if (dotLine instanceof ImageLine)
557 return;
558 if (editor.getBuffer().needsRenumbering())
559 editor.getBuffer().renumber();
560 if (dotLine.lineNumber() < topLine.lineNumber())
561 return;
562
563 int x;
564 if (caretCol == 0)
565 x = gutterWidth;
566 else if (dotLine.length() == 0)
567 x = gutterWidth + caretCol * spaceWidth;
568 else {
569 formatLine(dotLine, shift, caretCol);
570 x = gutterWidth + measureLine(g2d, textArray, caretCol, formatArray);
571 }
572
573 if (x > getWidth())
574 return;
575
576 int y = getY(dotLine);
577 if (y >= getHeight())
578 return;
579
580 g2d.setColor(editor.getFormatter().getCaretColor());
581
582 g2d.fillRect(x, y, 1, charAscent + charDescent);
584 }
585
586 public synchronized void setCaretVisible(boolean b)
587 {
588 caretVisible = b;
589 if (b && timer != null && timer.isRunning())
590 timer.restart();
591 }
592
593 private synchronized void blinkCaret()
594 {
595 Position dot = editor.getDot();
596 if (dot != null) {
597 caretVisible = !caretVisible;
598 final Line line = dot.getLine();
599 Runnable r = new Runnable () {
600 public void run()
601 {
602 repaintLine(line);
603 }
604 };
605 SwingUtilities.invokeLater(r);
606 }
607 }
608
609 private synchronized void repaintLine(Line l)
610 {
611 if (!Editor.displayReady())
612 return;
613 if ((updateFlag & REPAINT) == REPAINT) {
614 repaint();
615 return;
616 }
617 final Buffer buffer = editor.getBuffer();
618 initializePaint();
619 try {
620 buffer.lockRead();
621 }
622 catch (InterruptedException e) {
623 Log.error(e);
624 return;
625 }
626 try {
627 Graphics2D g2d = (Graphics2D ) getGraphics();
628 if (g2d != null) {
629 Line line = topLine;
630 int y = - pixelsAboveTopLine;
631 final int limit = getHeight();
632 while (line != null && y < limit) {
633 if (line == l) {
634 paintLine(line, g2d, y);
635 break;
636 }
637 y += line.getHeight();
638 line = line.nextVisible();
639 }
640 drawCaret(g2d);
641 }
642 }
643 finally {
644 buffer.unlockRead();
645 }
646 }
647
648 public void actionPerformed(ActionEvent e)
650 {
651 blinkCaret();
652 }
653
654 public synchronized void focusGained(FocusEvent e)
655 {
656 if (timer != null)
657 timer.start();
658 }
659
660 public synchronized void focusLost(FocusEvent e)
661 {
662 if (timer != null)
663 timer.stop();
664 }
665
666 private int formatLine(final Line line, final int begin, final int maxCols)
667 {
668 final int[] fa = formatArray;
670 final char[] ta = textArray;
671 final int taLength = ta.length;
672 Debug.assertTrue(taLength == fa.length);
673 for (int i = taLength; i-- > 0;) {
674 ta[i] = ' ';
675 fa[i] = 0;
676 }
677 final int limit = Math.min(maxCols, taLength);
678 final LineSegmentList segmentList = editor.getFormatter().formatLine(line);
679 int segmentStart = 0;
680 int totalChars = 0;
681 final int size = segmentList.size();
682 for (int i = 0; i < size; i++) {
683 final LineSegment segment = segmentList.getSegment(i);
684 final int segmentLength = segment.length();
685 if (segmentStart + segmentLength < begin) {
686 segmentStart += segmentLength;
687 continue;
688 }
689 final int maxAppend = limit - totalChars;
690 if (segmentStart >= begin) {
691 if (segmentLength <= maxAppend) {
692 segment.getChars(0, segmentLength, ta, totalChars);
693 totalChars += segmentLength;
694 } else if (maxAppend > 0) {
695 segment.getChars(0, maxAppend, ta, totalChars);
696 totalChars += maxAppend;
697 }
698 } else {
699 String text = segment.substring(begin - segmentStart);
701 if (text.length() <= maxAppend) {
702 text.getChars(0, text.length(), ta, totalChars);
703 totalChars += text.length();
704 } else if (maxAppend > 0) {
705 text.getChars(0, maxAppend, ta, totalChars);
706 totalChars += maxAppend;
707 }
708 }
709 final int format = segment.getFormat();
710 int k = segmentStart - begin;
711 if (k > limit)
712 break;
713 for (int j = 0; j < segmentLength; j++, k++) {
714 if (k >= 0 && k < limit)
715 fa[k] = format;
716 }
717 segmentStart += segmentLength;
718 }
719 return totalChars;
720 }
721
722 private Image paintLineImage;
723 private int paintLineImageWidth;
724 private int paintLineImageHeight;
725 private Graphics2D paintLineGraphics;
726
727 private final void providePaintLineImage(int width, int height)
728 {
729 if (paintLineImage != null &&
730 paintLineImageWidth == width &&
731 paintLineImageHeight == height)
732 return;
733
734 paintLineImage = createImage(width, height);
736 paintLineImageWidth = width;
737 paintLineImageHeight = height;
738 paintLineGraphics = (Graphics2D ) paintLineImage.getGraphics();
739
740 if (antialias) {
741 paintLineGraphics.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING,
742 RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
743 }
744 }
745
746 private final void paintLine(Line line, Graphics2D g2d, int y)
747 {
748 if (line instanceof ImageLine)
749 paintImageLine((ImageLine)line, g2d, y);
750 else
751 paintTextLine(line, g2d, y);
752 }
753
754 private synchronized void paintTextLine(Line line, Graphics g, int y)
755 {
756 int displayWidth = getWidth();
757 int maxCols = getMaxCols();
758
759 providePaintLineImage(displayWidth, charHeight);
760
761 Color backgroundColor;
762 if (line == getCurrentLine())
763 backgroundColor = editor.getFormatter().getCurrentLineBackgroundColor();
764 else
765 backgroundColor = editor.getFormatter().getBackgroundColor();
766 drawBackgroundForLine(paintLineGraphics, backgroundColor, line, 0);
767
768 int totalChars = formatLine(line, shift, maxCols);
769
770 if (editor.getMark() != null) {
771 Region r = new Region(editor);
773 handleSelection(r, line, formatArray, paintLineGraphics, 0);
774 } else if (posMatch != null) {
775 if (posMatch.getLine() == line)
776 highlightBracket(posMatch, line, formatArray,
777 paintLineGraphics, 0);
778 if (posBracket != null && posBracket.getLine() == line)
779 highlightBracket(posBracket, line, formatArray,
780 paintLineGraphics, 0);
781 }
782
783 drawGutterText(paintLineGraphics, line, 0);
784 if (showLineNumbers && editor.getDot() != null)
785 drawGutterBorder(paintLineGraphics, 0, line.getHeight());
786 drawVerticalRule(paintLineGraphics, 0, line.getHeight());
787 drawText(paintLineGraphics, textArray, totalChars, formatArray, 0);
788 changedLines.remove(line);
789
790 g.drawImage(paintLineImage, 0, y, null);
791 }
792
793 private void paintImageLine(ImageLine imageLine, Graphics g, int y)
794 {
795 final int displayWidth = getWidth();
796 final int lineHeight = imageLine.getHeight();
797 final int imageWidth = imageLine.getImageWidth();
798 final int imageHeight = imageLine.getImageHeight();
799 final int x = gutterWidth - shift * charWidth;
800
801 Color backgroundColor;
802 if (imageLine == getCurrentLine())
803 backgroundColor = editor.getFormatter().getCurrentLineBackgroundColor();
804 else
805 backgroundColor = editor.getFormatter().getBackgroundColor();
806
807 g.setColor(backgroundColor);
808 g.fillRect(0, y, x, lineHeight);
810 g.fillRect(x + imageWidth, y, displayWidth - (x + imageWidth), lineHeight);
812 if (imageHeight < lineHeight)
814 g.fillRect(0, y + imageHeight, displayWidth,
815 lineHeight - imageHeight);
816
817 Rectangle rect = imageLine.getRect();
818 g.drawImage(imageLine.getImage(),
819 x, y, x + rect.width, y + rect.height,
820 rect.x, rect.y, rect.x + rect.width, rect.y + rect.height,
821 null);
822 }
823
824 private void drawBackgroundForLine(Graphics2D g2d, Color backgroundColor,
825 Line line, int y)
826 {
827 if (enableChangeMarks && line.isModified()) {
828 g2d.setColor(line.isSaved() ? savedChangeColor : changeColor);
829 g2d.fillRect(0, y, changeMarkWidth, line.getHeight());
830 g2d.setColor(backgroundColor);
831 g2d.fillRect(changeMarkWidth, y, getWidth() - changeMarkWidth, line.getHeight());
832 } else {
833 g2d.setColor(backgroundColor);
834 g2d.fillRect(0, y, getWidth(), line.getHeight());
835 }
836 }
837
838 private void drawGutterText(Graphics g, Line line, int y)
839 {
840 int x = showChangeMarks ? changeMarkWidth : 0;
841 char c = 0;
842 Annotation annotation = line.getAnnotation();
843 if (annotation != null)
844 c = annotation.getGutterChar();
845 else if (line.next() != null && line.next().isHidden())
846 c = '+';
847 if (c != 0) {
848 char[] chars = new char[1];
849 chars[0] = c;
850 g.setColor(editor.getFormatter().getColor(0)); g.setFont(plainFont);
852 g.drawChars(chars, 0, 1, x, y + charAscent);
853 }
854 x += charWidth;
855 if (showLineNumbers) {
856 final String s = String.valueOf(line.lineNumber() + 1);
857 final int pad = MAX_LINE_NUMBER_CHARS - s.length();
858 if (pad >= 0) {
859 x += pad * gutterCharWidth;
860 g.setColor(lineNumberColor);
861 g.setFont(gutterFont);
862 g.drawString(s, x, y + charAscent);
863 }
864 }
865 }
866
867 private void drawGutterBorder(Graphics g)
868 {
869 int x = getGutterWidth(editor.getBuffer()) - 4;
870 g.setColor(gutterBorderColor);
871 g.drawLine(x, 0, x, getHeight());
872 }
873
874 private void drawGutterBorder(Graphics g, int y, int height)
875 {
876 int x = getGutterWidth(editor.getBuffer()) - 4;
877 g.setColor(gutterBorderColor);
878 g.drawLine(x, y, x, y + height);
879 }
880
881 public static final int getGutterWidth(Buffer buffer)
883 {
884 return getGutterWidth(buffer.getBooleanProperty(Property.SHOW_CHANGE_MARKS),
885 buffer.getBooleanProperty(Property.SHOW_LINE_NUMBERS));
886 }
887
888 private static final int getGutterWidth(boolean showChangeMarks,
890 boolean showLineNumbers)
891 {
892 int width = charWidth;
893 if (showChangeMarks)
894 width += changeMarkWidth;
895 if (showLineNumbers)
896 width += MAX_LINE_NUMBER_CHARS * gutterCharWidth + 5;
897 return width;
898 }
899
900 private void drawText(Graphics2D g2d, char[] textArray, int length,
901 int[] formatArray, int y)
902 {
903 int i = 0;
904 double x = gutterWidth;
905 final Formatter formatter = editor.getFormatter();
906 while (i < length) {
907 int format = formatArray[i];
908 int start = i;
909 while (formatArray[i] == format && i < length)
910 ++i;
911 int style;
912 FormatTableEntry entry = formatter.getFormatTableEntry(format);
913 if (entry != null) {
914 g2d.setColor(entry.getColor());
915 style = entry.getStyle();
916 } else {
917 g2d.setColor(formatter.getColor(format));
919 style = formatter.getStyle(format);
920 }
921 Font font;
922 switch (style) {
923 case Font.BOLD:
924 font = boldFont;
925 break;
926 case Font.ITALIC:
927 font = italicFont;
928 break;
929 case Font.PLAIN:
930 default:
931 font = plainFont;
932 break;
933 }
934 char[] chars = new char[i - start];
935 System.arraycopy(textArray, start, chars, 0, i - start);
936 GlyphVector gv = font.createGlyphVector(g2d.getFontRenderContext(), chars);
937 final double width = gv.getLogicalBounds().getWidth();
938 if (style == Font.BOLD) {
939 if (boldFont == plainFont) {
940 if (underlineBold)
941 g2d.drawLine((int)x, y + charAscent + 1, (int)(x + width), y + charAscent + 1);
942 else
943 g2d.drawGlyphVector(gv, (int)x + 1, y + charAscent);
944 } else if (emulateBold)
945 g2d.drawGlyphVector(gv, (float)x + 1, y + charAscent);
946 }
947 if (formatter.getUnderline(format))
948 g2d.drawLine((int)x, y + charAscent + 1, (int)(x + width), y + charAscent + 1);
949 g2d.drawGlyphVector(gv, (float)x, y + charAscent);
950 x += width;
951 }
952 }
953
954 private int measureLine(Graphics2D g2d, char[] textArray, int length, int[] formatArray)
955 {
956 if (length == 0)
957 return 0;
958 final int limit = Math.min(length, textArray.length);
959 double totalWidth = 0;
960 int i = 0;
961 Formatter formatter = editor.getFormatter();
962 while (i < limit) {
963 int format = formatArray[i];
964 int startCol = i;
965 while (i < limit && formatArray[i] == format)
966 ++i;
967 Font font;
968 switch (formatter.getStyle(format)) {
969 case Font.BOLD:
970 font = boldFont;
971 break;
972 case Font.ITALIC:
973 font = italicFont;
974 break;
975 case Font.PLAIN:
976 default:
977 font = plainFont;
978 break;
979 }
980 char[] chars = new char[i - startCol];
981 System.arraycopy(textArray, startCol, chars, 0, i - startCol);
982 GlyphVector gv = font.createGlyphVector(g2d.getFontRenderContext(), chars);
983 totalWidth += gv.getLogicalBounds().getWidth();
984 }
985 return (int) totalWidth;
986 }
987
988 public void paintComponent(Graphics g)
989 {
990 final Buffer buffer = editor.getBuffer();
991 if (!Editor.displayReady()) {
992 if (buffer != null && buffer.getModeId() == IMAGE_MODE)
993 g.setColor(ImageBuffer.getDefaultBackgroundColor());
994 else
995 g.setColor(editor.getFormatter().getBackgroundColor());
996 g.fillRect(0, 0, getWidth(), getHeight());
997 return;
998 }
999 try {
1000 buffer.lockRead();
1001 }
1002 catch (InterruptedException e) {
1003 Log.error(e);
1004 return;
1005 }
1006 try {
1007 if (buffer.getModeId() == IMAGE_MODE)
1008 paintImage(g);
1009 else
1010 paintComponentInternal(g);
1011 }
1012 finally {
1013 buffer.unlockRead();
1014 }
1015 }
1016
1017 private void paintImage(Graphics g)
1018 {
1019 ImageBuffer ib = (ImageBuffer) editor.getBuffer();
1020 g.setColor(ib.getBackgroundColor());
1021 g.fillRect(0, 0, getWidth(), getHeight());
1022 Image image = ib.getImage();
1023 if (image != null) {
1024 int imageWidth = image.getWidth(null);
1025 int imageHeight = image.getHeight(null);
1026 int x = 0;
1027 int y = 0;
1028 if (imageWidth > 0 && imageHeight > 0) {
1029 if (imageWidth < getWidth())
1030 x = (getWidth() - imageWidth) / 2;
1031 if (imageHeight < getHeight())
1032 y = (getHeight() - imageHeight) / 2;
1033 }
1034 if (x < getImageBorderWidth())
1035 x = getImageBorderWidth();
1036 if (y < getImageBorderHeight())
1037 y = getImageBorderHeight();
1038 g.drawImage(image, x - shift * charWidth, y - pixelsAboveTopLine, this);
1039 }
1040 }
1041
1042 private synchronized void paintComponentInternal(Graphics g)
1043 {
1044 initializePaint();
1045 Graphics2D g2d = (Graphics2D ) g;
1046 if (antialias) {
1047 g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING,
1048 RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
1049 }
1050 final Rectangle clipBounds = g2d.getClipBounds();
1051 final int displayWidth = getWidth();
1052 final int maxCols = getMaxCols();
1053
1054 final Region r = editor.getMark() != null ? new Region(editor) : null;
1056
1057 final Line currentLine = getCurrentLine();
1059
1060 final Color colorBackground = editor.getFormatter().getBackgroundColor();
1061 int y = - pixelsAboveTopLine;
1062 Line line = topLine;
1063 while (line != null && y + line.getHeight() < clipBounds.y) {
1064 y += line.getHeight();
1065 line = line.nextVisible();
1066 }
1067 final int limit = clipBounds.y + clipBounds.height;
1068 while (line != null && y < limit) {
1069 if (line instanceof ImageLine) {
1070 paintImageLine((ImageLine)line, g2d, y);
1071 } else {
1072 Color backgroundColor;
1073 if (line == currentLine) {
1074 backgroundColor =
1075 editor.getFormatter().getCurrentLineBackgroundColor();
1076 } else
1077 backgroundColor = colorBackground;
1078 drawBackgroundForLine(g2d, backgroundColor, line, y);
1079 int totalChars = formatLine(line, shift, maxCols);
1080 if (r != null)
1081 handleSelection(r, line, formatArray, g2d, y);
1082 else if (posMatch != null) {
1083 if (posMatch.getLine() == line)
1084 highlightBracket(posMatch, line, formatArray, g2d, y);
1085 if (posBracket != null && posBracket.getLine() == line)
1086 highlightBracket(posBracket, line, formatArray, g2d, y);
1087 }
1088 drawGutterText(g2d, line, y);
1089 if (totalChars > 0) {
1090 drawVerticalRule(g2d, y, line.getHeight());
1092 drawText(g2d, textArray, totalChars, formatArray, y);
1093 } else
1094 drawVerticalRule(g2d, y, line.getHeight());
1095 changedLines.remove(line);
1096 }
1097 y += line.getHeight();
1098 line = line.nextVisible();
1099 }
1100 if (y < limit) {
1101 g2d.setColor(colorBackground);
1102 g2d.fillRect(0, y, displayWidth, limit - y);
1103 drawVerticalRule(g2d, y, limit - y);
1104 }
1105 drawCaret(g2d);
1106 if (showLineNumbers && editor.getDot() != null)
1107 drawGutterBorder(g2d);
1108 updateFlag &= ~REPAINT;
1109 }
1110
1111 private Line getCurrentLine()
1112 {
1113 if (editor.getDot() != null && editor.getMark() == null)
1114 return editor.getDotLine();
1115 return null;
1116 }
1117
1118 private void handleSelection(Region r, Line line, int[] formatArray,
1119 Graphics2D g2d, int y)
1120 {
1121 if (r == null)
1122 return;
1123
1124 int maxCols = getMaxCols();
1125 int fillHeight = charHeight;
1126 int fillWidth = 0;
1127 int beginCol = 0;
1128 int endCol = 0;
1129 int x = 0;
1130
1131 if (r.isColumnRegion()) {
1132 if (line.lineNumber() >= r.getBeginLineNumber() &&
1133 line.lineNumber() <= r.getEndLineNumber()) {
1134 beginCol = r.getBeginCol() - shift;
1135 endCol = r.getEndCol() - shift;
1136
1137 if (beginCol < 0)
1138 beginCol = 0;
1139 if (endCol < 0)
1140 endCol = 0;
1141 if (endCol > maxCols)
1142 endCol = maxCols;
1143
1144 int x1 = measureLine(g2d, textArray, beginCol, formatArray);
1145 int x2 = measureLine(g2d, textArray, endCol, formatArray);
1146 fillWidth = x2 - x1;
1147 x = gutterWidth + x1;
1148 }
1149 } else if (line == r.getBeginLine()) {
1150 beginCol = r.getBeginCol() - shift;
1151 if (line == r.getEndLine())
1152 endCol = r.getEndCol() - shift;
1153
1154 if (beginCol < 0)
1155 beginCol = 0;
1156 if (endCol < 0)
1157 endCol = 0;
1158 if (endCol > maxCols)
1159 endCol = maxCols;
1160
1161 if (line == r.getEndLine()) {
1162 int x1 = measureLine(g2d, textArray, beginCol, formatArray);
1163 int x2 = measureLine(g2d, textArray, endCol, formatArray);
1164 fillWidth = x2 - x1;
1165 x = gutterWidth + x1;
1166 } else {
1167 fillWidth = getWidth();
1168 x = gutterWidth + measureLine(g2d, textArray, beginCol, formatArray);
1169 }
1170 } else if (line.lineNumber() > r.getBeginLineNumber() &&
1171 line.lineNumber() < r.getEndLineNumber()) {
1172 fillWidth = getWidth();
1174 x = gutterWidth;
1175 } else if (line == r.getEndLine()) {
1176 endCol = r.getEndCol() - shift;
1178
1179 if (endCol < 0)
1180 endCol = 0;
1181 if (endCol > maxCols)
1182 endCol = maxCols;
1183
1184 int x1 = measureLine(g2d, textArray, beginCol, formatArray);
1185 int x2 = measureLine(g2d, textArray, endCol, formatArray);
1186 fillWidth = x2 - x1;
1187 x = gutterWidth + x1;
1188 }
1189
1190 if (fillWidth > 0) {
1191 g2d.setColor(editor.getFormatter().getSelectionBackgroundColor());
1192 g2d.fillRect(x, y, fillWidth, charHeight);
1193 }
1194 }
1195
1196 private void highlightBracket(Position pos, Line line, int[] formatArray,
1197 Graphics2D g2d, int y)
1198 {
1199 if (pos == null) {
1200 Debug.bug();
1201 return;
1202 }
1203 if (pos.getLine() != line) {
1204 Debug.bug();
1205 return;
1206 }
1207 if (editor.getFrame().getFocusedComponent() != this)
1208 return;
1209 int beginCol = editor.getBuffer().getCol(pos) - shift;
1210 if (beginCol < 0)
1211 return;
1212 int endCol = beginCol + 1;
1213 int x1 = measureLine(g2d, textArray, beginCol, formatArray);
1214 int x2 = measureLine(g2d, textArray, endCol, formatArray);
1215 int fillWidth = x2 - x1;
1216 int x = gutterWidth + x1;
1217 if (fillWidth > 0) {
1218 g2d.setColor(editor.getFormatter().getMatchingBracketBackgroundColor());
1219 g2d.fillRect(x, y, fillWidth, charHeight);
1220 }
1221 }
1222
1223 private void scrollUp()
1225 {
1226 if (editor.getModeId() == IMAGE_MODE) {
1227 if (pixelsAboveTopLine >= charHeight) {
1228 pixelsAboveTopLine -= charHeight;
1229 repaint();
1230 }
1231 return;
1232 }
1233
1234 if (topLine != null) {
1235 if (topLine instanceof ImageLine) {
1236 if (pixelsAboveTopLine - charHeight >= 0) {
1237 pixelsAboveTopLine -= charHeight;
1238 scrollPixelsUp(charHeight);
1239 Rectangle r = new Rectangle (0, 0, getWidth(), charHeight);
1240 paintImmediately(r);
1241 return;
1242 }
1243 }
1244 Line line = topLine.previousVisible();
1245 if (line == null)
1246 return;
1247 if (line instanceof ImageLine) {
1248 scrollPixelsUp(charHeight);
1249 topLine = line;
1250 pixelsAboveTopLine = line.getHeight() - charHeight;
1251 editor.update(topLine);
1252 return;
1253 }
1254 scrollPixelsUp(charHeight);
1255 setTopLine(line);
1256 editor.update(topLine);
1257 }
1258 }
1259
1260 private void scrollDown()
1262 {
1263 if (editor.getModeId() == IMAGE_MODE) {
1264 pixelsAboveTopLine += charHeight;
1265 repaint();
1266 return;
1267 }
1268 if (topLine != null) {
1269 if (topLine instanceof ImageLine) {
1270 if (pixelsAboveTopLine + charHeight < topLine.getHeight()) {
1271 pixelsAboveTopLine += charHeight;
1272 scrollPixelsDown(charHeight);
1273 Rectangle r = new Rectangle ();
1274 r.x = 0;
1275 r.y = getHeight() - charHeight;
1276 r.width = getWidth();
1277 r.height = charHeight;
1278 paintImmediately(r);
1279 return;
1280 }
1281 }
1282 Line line = topLine.nextVisible();
1283 if (line != null) {
1284 scrollPixelsDown(charHeight);
1285 setTopLine(line);
1286 Line bottomLine = getBottomLine();
1287 editor.update(bottomLine);
1288 Line nextVisible = bottomLine.nextVisible();
1289 if (nextVisible != null)
1290 editor.update(nextVisible);
1291 }
1292 }
1293 }
1294
1295 private void scrollPixelsUp(int dy)
1297 {
1298 Point pt1 = editor.getFrame().getLocationOnScreen();
1299 Point pt2 = getLocationOnScreen();
1300 int x = pt2.x - pt1.x;
1301 int y = pt2.y - pt1.y;
1302 editor.getFrame().getGraphics().copyArea(x, y, getWidth(),
1303 getHeight() - dy, 0, dy);
1304 }
1305
1306 private void scrollPixelsDown(int dy)
1308 {
1309 Point pt1 = editor.getFrame().getLocationOnScreen();
1310 Point pt2 = getLocationOnScreen();
1311 int x = pt2.x - pt1.x;
1312 int y = pt2.y - pt1.y + dy;
1313 editor.getFrame().getGraphics().copyArea(x, y, getWidth(),
1314 getHeight() - dy, 0, - dy);
1315 }
1316
1317 public Line getBottomLine()
1318 {
1319 Line line = topLine;
1320 int y = line.getHeight() - pixelsAboveTopLine;
1321 final int limit = getHeight();
1322 while (true) {
1323 Line next = line.nextVisible();
1324 if (next == null)
1325 break;
1326 y += next.getHeight();
1327 if (y > limit)
1328 break;
1329 line = next;
1330 }
1331 return line;
1332 }
1333
1334 public void up(boolean select)
1335 {
1336 if (editor.getDot() == null)
1337 return;
1338
1339 if (select) {
1340 if (editor.getMark() == null)
1341 editor.addUndo(SimpleEdit.MOVE);
1342 else if (editor.getLastCommand() != COMMAND_UP)
1343 editor.addUndo(SimpleEdit.MOVE);
1344 } else {
1345 if (editor.getMark() != null) {
1346 boolean isLineBlock =
1347 (editor.getDotOffset() == 0 && editor.getMarkOffset() == 0);
1348 editor.addUndo(SimpleEdit.MOVE);
1349 editor.beginningOfBlock();
1350 editor.setGoalColumn(editor.getDotCol());
1351 if (isLineBlock)
1352 return;
1353 } else if (editor.getLastCommand() != COMMAND_UP)
1354 editor.addUndo(SimpleEdit.MOVE);
1355 }
1356
1357 Line dotLine = editor.getDotLine();
1358 Line prevLine = dotLine.previousVisible();
1359 if (prevLine == null)
1360 return;
1361 if (dotLine == topLine) {
1362 windowUp();
1364 }
1365 editor.updateDotLine();
1366 final Buffer buffer = editor.getBuffer();
1367 boolean selectLine = false;
1368 if (select && editor.getMark() == null) {
1369 Position savedDot = null;
1370 if (buffer.getBooleanProperty(Property.AUTO_SELECT_LINE)) {
1371 Line nextLine = editor.getDotLine().next();
1372 if (nextLine != null) {
1373 selectLine = true;
1374 savedDot = new Position(editor.getDot());
1375 editor.getDot().moveTo(nextLine, 0);
1376 caretCol = 0;
1377 }
1378 }
1379 if (selectLine) {
1380 int savedShift = shift;
1382 shift = 0;
1383 editor.setMarkAtDot();
1384 shift = savedShift;
1385 } else
1386 editor.setMarkAtDot();
1387 if (savedDot != null)
1388 editor.getSelection().setSavedDot(savedDot);
1389 }
1390 editor.getDot().setLine(prevLine);
1391 editor.updateDotLine();
1392 if (selectLine)
1393 editor.setGoalColumn(0);
1394 editor.moveDotToGoalCol();
1395 }
1396
1397 public void down(boolean select)
1398 {
1399 if (editor.getDot() == null)
1400 return;
1401 if (select) {
1402 if (editor.getMark() == null)
1403 editor.addUndo(SimpleEdit.MOVE);
1404 else if (editor.getLastCommand() != COMMAND_DOWN)
1405 editor.addUndo(SimpleEdit.MOVE);
1406 } else {
1407 if (editor.getMark() != null) {
1408 boolean isLineBlock =
1409 (editor.getDotOffset() == 0 && editor.getMarkOffset() == 0);
1410 editor.addUndo(SimpleEdit.MOVE);
1411 editor.endOfBlock();
1412 editor.setGoalColumn(editor.getDotCol());
1413 if (isLineBlock)
1414 return;
1415 }
1416 else if (editor.getLastCommand() != COMMAND_DOWN)
1417 editor.addUndo(SimpleEdit.MOVE);
1418 }
1419 final Line dotLine = editor.getDotLine();
1420 final Line nextLine = dotLine.nextVisible();
1421 if (nextLine == null)
1422 return;
1423 if (getY(nextLine) + nextLine.getHeight() > getHeight()) {
1424 windowDown();
1426 }
1427 editor.updateDotLine();
1428 final Buffer buffer = editor.getBuffer();
1429 boolean selectLine = false;
1430 if (select && editor.getMark() == null) {
1431 Position savedDot = null;
1432 if (buffer.getBooleanProperty(Property.AUTO_SELECT_LINE)) {
1433 selectLine = true;
1434 savedDot = new Position(editor.getDot());
1435 editor.getDot().setOffset(0);
1436 caretCol = 0;
1437 }
1438 if (selectLine) {
1439 int savedShift = shift;
1441 shift = 0;
1442 editor.setMarkAtDot();
1443 shift = savedShift;
1444 } else
1445 editor.setMarkAtDot();
1446 if (savedDot != null)
1447 editor.getSelection().setSavedDot(savedDot);
1448 }
1449 editor.getDot().setLine(nextLine);
1450 editor.updateDotLine();
1451 if (selectLine)
1452 editor.setGoalColumn(0);
1453 editor.moveDotToGoalCol();
1454 }
1455
1456 public void windowUp()
1457 {
1458 if (getHeight() < editor.getBuffer().getDisplayHeight())
1459 scrollUp();
1460 }
1461
1462 public void windowDown()
1463 {
1464 final int totalHeight = editor.getBuffer().getDisplayHeight();
1465 final int windowHeight = getHeight();
1466 if (windowHeight < totalHeight) {
1467 int y;
1469 if (topLine != null)
1470 y = editor.getBuffer().getY(topLine) + pixelsAboveTopLine + windowHeight;
1471 else
1472 y = pixelsAboveTopLine + windowHeight;
1473 if (y < totalHeight)
1474 scrollDown();
1475 }
1476 }
1477
1478 public void windowUp(int lines)
1479 {
1480 Line line = topLine;
1481 if (line == null) {
1482 if (editor.getModeId() == IMAGE_MODE) {
1483 pixelsAboveTopLine -= lines * charHeight;
1484 if (pixelsAboveTopLine < 0)
1485 pixelsAboveTopLine = 0;
1486 repaint();
1487 }
1488 return;
1489 }
1490 if (line instanceof ImageLine) {
1491 imageLineWindowUp(lines);
1492 return;
1493 }
1494 int actual = 0;
1495 for (int i = 0; i < lines; i++) {
1496 Line prev = line.previousVisible();
1497 if (prev == null)
1498 break;
1499 if (prev instanceof ImageLine) {
1500 imageLineWindowUp(lines);
1501 return;
1502 }
1503 line = prev;
1504 lineChanged(line);
1505 ++actual;
1506 }
1507 scrollPixelsUp(actual * charHeight);
1508 setTopLine(line);
1509 editor.maybeScrollCaret();
1510 editor.updateDisplay();
1511 }
1512
1513 private void imageLineWindowUp(int lines)
1514 {
1515 int oldY = getAbsoluteY(topLine) + pixelsAboveTopLine;
1516 int newY = oldY - lines * charHeight;
1517 if (newY < 0)
1518 newY = 0;
1519 Line line = lineFromAbsoluteY(newY);
1520 if (line != null) {
1521 int y = getAbsoluteY(line);
1522 topLine = line;
1523 pixelsAboveTopLine = newY - y;
1524 setUpdateFlag(REPAINT);
1525 editor.updateDisplay();
1526 }
1527 }
1528
1529 public void windowDown(final int lines)
1530 {
1531 Line top = topLine;
1532 if (top == null) {
1533 if (editor.getModeId() == IMAGE_MODE) {
1534 int windowHeight = getHeight();
1535 int bufferHeight = editor.getBuffer().getDisplayHeight();
1536 pixelsAboveTopLine += lines * charHeight;
1537 if (pixelsAboveTopLine + windowHeight > bufferHeight)
1538 pixelsAboveTopLine = bufferHeight - windowHeight;
1539 repaint();
1540 }
1541 return;
1542 }
1543 if (top instanceof ImageLine) {
1544 imageLineWindowDown(lines);
1545 return;
1546 }
1547 int actual = 0;
1548 Line bottom = getBottomLine();
1549 for (int i = 0; i < lines; i++) {
1550 bottom = bottom.nextVisible();
1551 if (bottom == null)
1552 break;
1553 lineChanged(bottom);
1554 Line next = top.nextVisible();
1555 if (next instanceof ImageLine) {
1556 imageLineWindowDown(lines);
1557 return;
1558 }
1559 if (next == null)
1560 break;
1561 top = next;
1562 ++actual;
1563 }
1564 if (bottom != null) {
1565 bottom = bottom.nextVisible();
1566 if (bottom != null)
1567 lineChanged(bottom);
1568 }
1569 scrollPixelsDown(actual * charHeight);
1570 setTopLine(top);
1571 editor.maybeScrollCaret();
1572 editor.updateDisplay();
1573 }
1574
1575 private void imageLineWindowDown(int lines)
1576 {
1577 Line top = topLine;
1578 int oldY = getAbsoluteY(top) + pixelsAboveTopLine;
1579 int newY = oldY + lines * charHeight;
1580 int windowHeight = getHeight();
1581 int bufferHeight = editor.getBuffer().getDisplayHeight();
1582 if (newY + windowHeight > bufferHeight)
1583 newY = bufferHeight - windowHeight;
1584 if (newY == oldY)
1585 return;
1586 Line line = lineFromAbsoluteY(newY);
1587 if (line != null) {
1588 int y = getAbsoluteY(line);
1589 topLine = line;
1590 pixelsAboveTopLine = newY - y;
1591 setUpdateFlag(REPAINT);
1592 editor.updateDisplay();
1593 }
1594 }
1595
1596 public void setUpdateFlag(int mask)
1597 {
1598 updateFlag |= mask;
1599 }
1600
1601 private int reframeParam = 0;
1602
1603 public void setReframe(int n)
1604 {
1605 reframeParam = n;
1606 }
1607
1608 public void reframe()
1609 {
1610 if (!Editor.displayReady())
1611 return;
1612 if (editor.getDot() == null)
1613 return;
1614 if (getHeight() == 0)
1615 return; if (topLine == null || (updateFlag & REFRAME) != 0) {
1617 final Buffer buffer = editor.getBuffer();
1618 try {
1619 buffer.lockRead();
1620 }
1621 catch (InterruptedException e) {
1622 Log.error(e);
1623 return;
1624 }
1625 try {
1626 reframeHorizontally();
1627 reframeVertically();
1628 }
1629 finally {
1630 buffer.unlockRead();
1631 }
1632 updateFlag &= ~REFRAME;
1633 }
1634 }
1635
1636 private void reframeVertically()
1637 {
1638 if (topLine != null && topLine.isHidden()) {
1639 Line prev = topLine.previousVisible();
1640 setTopLine(prev != null ? prev : topLine.nextVisible());
1641 setUpdateFlag(REPAINT);
1642 }
1643
1644 if (topLine == null || mustReframe()) {
1645 Line top = findNewTopLine(editor.getDotLine());
1646 setTopLine(top);
1647 setUpdateFlag(REPAINT);
1648 }
1649
1650 reframeParam = 0;
1651
1652
1655 if (topLine.previousVisible() == null)
1657 return;
1658
1659 int y = getAbsoluteY(topLine);
1660 int limit =
1661 editor.getBuffer().getDisplayHeight() - getHeight() + charHeight;
1662 if (y > limit) {
1663 Line top = lineFromAbsoluteY(limit);
1665 setTopLine(top);
1666 setUpdateFlag(REPAINT);
1667 reframeParam = 0;
1668 }
1669 }
1670
1671 private boolean mustReframe()
1673 {
1674 final int height = getHeight();
1675 final Line dotLine = editor.getDotLine();
1676 Line line = topLine;
1677 int y = - pixelsAboveTopLine;
1678 while (y < height) {
1679 if (line == dotLine) {
1680 return y + line.getHeight() > height;
1682 }
1683 Line next = line.nextVisible();
1684 if (next == null)
1685 return true;
1686 y += line.getHeight();
1687 line = next;
1688 }
1689 return true;
1690 }
1691
1692 private Line findNewTopLine(final Line dotLine)
1694 {
1695 int y;
1696 if (reframeParam == 0)
1697 y = getHeight() / 2; else if (reframeParam > 0)
1699 y = (reframeParam - 1) * charHeight;
1700 else y = getHeight() + reframeParam * charHeight;
1702
1703 Line line = dotLine;
1704 while (true) {
1705 Line prev = line.previousVisible();
1706 if (prev == null)
1707 break;
1708 y -= prev.getHeight();
1709 if (y < 0)
1710 break;
1711 line = prev;
1712 }
1713
1714 return line;
1715 }
1716
1717 private void reframeHorizontally()
1718 {
1719 if (editor.getDot() == null)
1720 return;
1721 if (editor.getDotLine() instanceof ImageLine)
1722 return;
1723 final int absCaretCol = caretCol + shift;
1724 Debug.assertTrue(absCaretCol >= 0);
1725 ensureColumnVisible(editor.getDotLine(), absCaretCol);
1726 caretCol = absCaretCol - shift;
1727 }
1728
1729 public synchronized void ensureColumnVisible(Line line, int absCol)
1730 {
1731 final int oldShift = shift;
1732 if (absCol < 50)
1733 shift = 0;
1734 int col = absCol - shift;
1735 if (col < 0) {
1736 do {
1737 shift -= 8;
1738 if (shift < 0)
1739 shift = 0;
1740 col = absCol - shift;
1741 } while (col < 0);
1742 } else {
1743 if (col > getMaxCols()) {
1744 shift = absCol - getMaxCols();
1745 col = absCol - shift;
1746 Debug.assertTrue(col == getMaxCols());
1747 }
1748 Graphics2D g2d = (Graphics2D ) getGraphics();
1749 if (g2d == null) {
1750 Log.error("ensureColumnVisible g2d is null");
1751 return;
1752 }
1753 formatLine(line, shift, col);
1754 int x = measureLine(g2d, textArray, col, formatArray);
1755 final int maxWidth = getWidth() - gutterWidth - charWidth;
1756 while (x > maxWidth) {
1757 shift += 8;
1758 col = absCol - shift;
1759 formatLine(line, shift, col);
1760 x = measureLine(g2d, textArray, col, formatArray);
1761 }
1762 }
1763 if (shift != oldShift)
1764 setUpdateFlag(REPAINT);
1765 }
1766
1767 public void toCenter()
1768 {
1769 Line line = editor.getDotLine();
1770 int limit = getRows() / 2;
1771 for (int i = 0; i < limit; i++) {
1772 Line prev = line.previousVisible();
1773 if (prev == null)
1774 break;
1775 line = prev;
1776 }
1777 setTopLine(line);
1778 setUpdateFlag(REPAINT);
1779 }
1780
1781 public void toTop()
1782 {
1783 Line goal = editor.getDotLine().previousVisible();
1784 if (goal == null)
1785 goal = editor.getDotLine();
1786 if (topLine != goal) {
1787 setTopLine(goal);
1788 setUpdateFlag(REPAINT);
1789 }
1790 }
1791
1792 public void centerRegion(Line begin, Line end)
1794 {
1795 if (begin == null)
1796 return;
1797 if (end != null) {
1798 if (isLineVisible(begin) && isLineVisible(end))
1799 return; }
1801 Line newTopLine = null;
1802 int linesInRegion = 0;
1803 if (end != null) {
1804 for (Line line = begin; line != null && line.isBefore(end); line = line.nextVisible())
1805 ++linesInRegion;
1806 } else {
1807 for (Line line = begin; line != null; line = line.nextVisible())
1808 ++linesInRegion;
1809 }
1810 int numRows = getRows();
1811 if (numRows > linesInRegion) {
1812 int linesAbove = (numRows - linesInRegion) / 2;
1813 newTopLine = begin;
1814 do {
1815 Line prev = newTopLine.previousVisible();
1816 if (prev != null)
1817 newTopLine = prev;
1818 else
1819 break;
1820 --linesAbove;
1821 }
1822 while (linesAbove > 0);
1823 }
1824 if (newTopLine == null) {
1825 Line prev = begin.previousVisible();
1826 newTopLine = prev != null ? prev : begin;
1827 }
1828 if (topLine != newTopLine) {
1829 setTopLine(newTopLine);
1830 setUpdateFlag(REPAINT);
1831 }
1832 }
1833
1834 private boolean isLineVisible(Line line)
1835 {
1836 return (line.lineNumber() >= getTopLineNumber() &&
1837 line.lineNumber() < getTopLineNumber() + getRows());
1838 }
1839
1840 private final int getMaxCols()
1841 {
1842 return (getWidth() / charWidth) * 5 / 4;
1845 }
1846
1847 public final int getColumns()
1848 {
1849 return (getWidth()-getGutterWidth(editor.getBuffer()))/charWidth - 1;
1850 }
1851
1852 public final int getRows()
1853 {
1854 return getHeight() / charHeight;
1855 }
1856
1857 public void moveCaretToPoint(Point point)
1858 {
1859 final Position dot = editor.getDot();
1860 if (dot == null)
1861 return;
1862 final Line line = lineFromY(point.y);
1863 if (line == null)
1864 return;
1865 if (line != dot.getLine()) {
1866 editor.updateDotLine();
1867 dot.setLine(line);
1868 }
1869 caretCol = Math.max(getColumn(line, point.x), 0);
1870 editor.moveDotToCol(caretCol + shift);
1871 }
1872
1873 public synchronized Position positionFromPoint(Point point, int shift)
1874 {
1875 int savedShift = this.shift;
1876 this.shift = shift;
1877 Position pos = positionFromPoint(point);
1878 this.shift = savedShift;
1879 return pos;
1880 }
1881
1882 public Position positionFromPoint(Point point)
1883 {
1884 return positionFromPoint(point.x, point.y);
1885 }
1886
1887 public Position positionFromPoint(int x, int y)
1888 {
1889 Line line = lineFromY(y);
1890 if (line == null)
1891 return null;
1892 Position pos = new Position(line, 0);
1893 int col = getColumn(line, x);
1894 pos.moveToCol(col + shift, editor.getBuffer().getTabWidth());
1895 return pos;
1896 }
1897
1898 public Line lineFromY(int y)
1900 {
1901 if (topLine == null)
1902 return null;
1903 Line line = topLine;
1904 int total = - pixelsAboveTopLine;
1905 final int limit = getHeight();
1906 while (true) {
1907 total += line.getHeight();
1908 if (total > y)
1909 break;
1910 if (total > limit)
1911 break;
1912 Line next = line.nextVisible();
1913 if (next == null)
1914 break;
1915 line = next;
1916 }
1917 return line;
1918 }
1919
1920 private Line lineFromAbsoluteY(int y)
1922 {
1923 Line line = editor.getBuffer().getFirstLine();
1924 if (line != null) {
1925 int total = 0;
1926 while (true) {
1927 total += line.getHeight();
1928 if (total > y)
1929 break;
1930 Line next = line.nextVisible();
1931 if (next != null)
1932 line = line.nextVisible();
1933 else
1934 break;
1935 }
1936 }
1937 return line;
1938 }
1939
1940 public synchronized int getColumn(Line line, int x)
1941 {
1942 if (line instanceof ImageLine)
1943 return 0;
1944 int maxCols = getMaxCols();
1945 formatLine(line, shift, maxCols);
1946 Graphics2D g2d = (Graphics2D ) getGraphics();
1947 int begin = 0;
1948 int end = maxCols;
1949 while (end - begin > 4) {
1950 int pivot = (begin + end) / 2;
1951 int width = measureLine(g2d, textArray, pivot, formatArray);
1952 if (width + gutterWidth > x)
1953 end = pivot + 1;
1954 else
1955 begin = pivot - 1;
1956 }
1957 for (int i = begin; i < end; i++) {
1958 int width = measureLine(g2d, textArray, i, formatArray);
1959 if (width + gutterWidth > x)
1960 return i - 1;
1961 }
1962 return 0; }
1964
1965 public boolean isOpaque()
1966 {
1967 return true;
1968 }
1969
1970 public synchronized final void lineChanged(Line line)
1971 {
1972 if (line == null) {
1974 Debug.bug("lineChanged line is null");
1975 return;
1976 }
1977 changedLines.put(line, line);
1978 }
1979
1980 public static void resetDisplay()
1981 {
1982 if (plainFont == null)
1983 return; initializeStaticValues();
1985 for (EditorIterator it = new EditorIterator(); it.hasNext();) {
1986 Display display = it.nextEditor().getDisplay();
1987 display.initialize();
1988 display.repaint();
1989 }
1990 }
1991
1992 public static void setRenderingHints(Graphics g)
1993 {
1994 if (antialias) {
1995 Graphics2D g2d = (Graphics2D ) g;
1996 g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING,
1997 RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
1998 }
1999 }
2000
2001 public String getToolTipText(MouseEvent e)
2002 {
2003 return editor.getMode().getToolTipText(editor, e);
2004 }
2005}
2006 |
Popular Tags |
Java API By Example, From Geeks To Geeks.