0001: /*
0002: * Display.java
0003: *
0004: * Copyright (C) 1998-2004 Peter Graves
0005: * $Id: Display.java,v 1.17 2004/04/01 18:48:42 piso Exp $
0006: *
0007: * This program is free software; you can redistribute it and/or
0008: * modify it under the terms of the GNU General Public License
0009: * as published by the Free Software Foundation; either version 2
0010: * of the License, or (at your option) any later version.
0011: *
0012: * This program is distributed in the hope that it will be useful,
0013: * but WITHOUT ANY WARRANTY; without even the implied warranty of
0014: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0015: * GNU General Public License for more details.
0016: *
0017: * You should have received a copy of the GNU General Public License
0018: * along with this program; if not, write to the Free Software
0019: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
0020: */
0021:
0022: package org.armedbear.j;
0023:
0024: import java.awt.Color;
0025: import java.awt.Font;
0026: import java.awt.FontMetrics;
0027: import java.awt.Graphics2D;
0028: import java.awt.Graphics;
0029: import java.awt.Image;
0030: import java.awt.Point;
0031: import java.awt.Rectangle;
0032: import java.awt.RenderingHints;
0033: import java.awt.Toolkit;
0034: import java.awt.event.ActionEvent;
0035: import java.awt.event.ActionListener;
0036: import java.awt.event.FocusEvent;
0037: import java.awt.event.FocusListener;
0038: import java.awt.event.MouseEvent;
0039: import java.awt.font.GlyphVector;
0040: import java.util.HashMap;
0041: import javax.swing.JComponent;
0042: import javax.swing.SwingUtilities;
0043: import javax.swing.Timer;
0044:
0045: public final class Display extends JComponent implements Constants,
0046: ActionListener, FocusListener {
0047: private static final int MAX_LINE_NUMBER_CHARS = 6;
0048:
0049: private static final Preferences preferences = Editor.preferences();
0050:
0051: private static Font plainFont;
0052: private static Font boldFont;
0053: private static Font italicFont;
0054:
0055: private static int charHeight;
0056: private static int charDescent;
0057: private static int charAscent;
0058: private static int charLeading;
0059: private static int charWidth;
0060: private static int spaceWidth; // Width of a space character.
0061: private static int minCharWidth;
0062:
0063: private static boolean antialias;
0064: private static boolean underlineBold;
0065: private static boolean emulateBold;
0066:
0067: private static int changeMarkWidth;
0068:
0069: private static Font gutterFont;
0070: private static int gutterCharAscent;
0071: private static int gutterCharWidth;
0072:
0073: private static boolean showGutterBorder = true;
0074:
0075: private static int leftMargin;
0076:
0077: private final HashMap changedLines = new HashMap();
0078:
0079: private final Editor editor;
0080:
0081: private Line topLine;
0082: private int pixelsAboveTopLine;
0083:
0084: // The offset of the first visible column of the display.
0085: int shift = 0;
0086:
0087: // The column containing the caret, relative to the first visible column
0088: // of the display. The absolute column number will be different if we're
0089: // horizontally scrolled (absolute column number = caretCol + shift).
0090: int caretCol;
0091:
0092: private char[] textArray;
0093: private int[] formatArray;
0094:
0095: private int updateFlag;
0096:
0097: // These are set in initializePaint().
0098: private boolean showChangeMarks;
0099: private boolean enableChangeMarks;
0100: private boolean showLineNumbers;
0101: private int gutterWidth;
0102: private Color changeColor;
0103: private Color savedChangeColor;
0104: private Color lineNumberColor;
0105: private int verticalRuleX;
0106: private Color verticalRuleColor;
0107: private Color gutterBorderColor;
0108: private boolean highlightBrackets;
0109: private boolean highlightMatchingBracket;
0110: private Position posBracket;
0111: private Position posMatch;
0112:
0113: private Timer timer;
0114: private boolean caretVisible = true;
0115:
0116: public Display(Editor editor) {
0117: this .editor = editor;
0118: if (plainFont == null)
0119: initializeStaticValues();
0120: initialize();
0121: setFocusTraversalKeysEnabled(false);
0122: setToolTipText("");
0123: }
0124:
0125: public static void initializeStaticValues() {
0126: final String fontName = preferences
0127: .getStringProperty(Property.FONT_NAME);
0128: final int fontSize = preferences
0129: .getIntegerProperty(Property.FONT_SIZE);
0130:
0131: plainFont = new Font(fontName, Font.PLAIN, fontSize);
0132: boldFont = new Font(fontName, Font.BOLD, fontSize);
0133: if (preferences.getBooleanProperty(Property.ENABLE_ITALICS))
0134: italicFont = new Font(fontName, Font.ITALIC, fontSize);
0135: else
0136: italicFont = plainFont;
0137:
0138: FontMetrics fm = Toolkit.getDefaultToolkit().getFontMetrics(
0139: plainFont);
0140:
0141: final int plainAscent = fm.getAscent();
0142: final int plainDescent = fm.getDescent();
0143: final int plainLeading = fm.getLeading();
0144:
0145: charWidth = fm.charWidth('a');
0146: spaceWidth = fm.charWidth(' ');
0147: minCharWidth = getMinCharWidth(fm);
0148:
0149: leftMargin = charWidth;
0150:
0151: fm = Toolkit.getDefaultToolkit().getFontMetrics(boldFont);
0152:
0153: final int boldAscent = fm.getAscent();
0154: final int boldDescent = fm.getDescent();
0155: final int boldLeading = fm.getLeading();
0156:
0157: charAscent = plainAscent;
0158: if (boldAscent > charAscent)
0159: charAscent = boldAscent;
0160:
0161: charDescent = plainDescent;
0162: if (boldDescent > charDescent)
0163: charDescent = boldDescent;
0164:
0165: // Use no more than 1 pixel of leading.
0166: charLeading = (plainLeading > 0 || boldLeading > 0) ? 1 : 0;
0167:
0168: // Apply user-specified adjustments.
0169: final int adjustAscent = preferences
0170: .getIntegerProperty(Property.ADJUST_ASCENT);
0171: final int adjustDescent = preferences
0172: .getIntegerProperty(Property.ADJUST_DESCENT);
0173: final int adjustLeading = preferences
0174: .getIntegerProperty(Property.ADJUST_LEADING);
0175:
0176: if (charAscent + adjustAscent >= 0)
0177: charAscent += adjustAscent;
0178: if (charDescent + adjustDescent >= 0)
0179: charDescent += adjustDescent;
0180: if (charLeading + adjustLeading >= 0)
0181: charLeading += adjustLeading;
0182:
0183: charHeight = charAscent + charDescent + charLeading;
0184:
0185: antialias = preferences.getBooleanProperty(Property.ANTIALIAS);
0186: underlineBold = preferences
0187: .getBooleanProperty(Property.UNDERLINE_BOLD);
0188: emulateBold = preferences
0189: .getBooleanProperty(Property.EMULATE_BOLD);
0190:
0191: String gutterFontName = preferences
0192: .getStringProperty(Property.GUTTER_FONT_NAME);
0193: if (gutterFontName == null)
0194: gutterFontName = fontName;
0195: int gutterFontSize = preferences
0196: .getIntegerProperty(Property.GUTTER_FONT_SIZE);
0197: if (gutterFontSize == 0)
0198: gutterFontSize = fontSize;
0199: gutterFont = new Font(gutterFontName, Font.PLAIN,
0200: gutterFontSize);
0201:
0202: fm = Toolkit.getDefaultToolkit().getFontMetrics(gutterFont);
0203: gutterCharAscent = fm.getAscent();
0204: gutterCharWidth = fm.charWidth('0');
0205:
0206: changeMarkWidth = preferences
0207: .getIntegerProperty(Property.CHANGE_MARK_WIDTH);
0208: }
0209:
0210: public synchronized void initialize() {
0211: // Explicitly set this to null here. We might be resetting the display.
0212: paintLineImage = null;
0213:
0214: // Allocate text and format arrays big enough to handle full screen
0215: // width for narrowest character in font, plus some slack (runs of
0216: // italics tend to get compressed). An extra 25% should be plenty.
0217: int size = Toolkit.getDefaultToolkit().getScreenSize().width
0218: * 5 / (minCharWidth * 4);
0219: textArray = new char[size];
0220: formatArray = new int[size];
0221:
0222: if (preferences.getBooleanProperty(Property.BLINK_CARET)) {
0223: if (timer == null) {
0224: timer = new Timer(500, this );
0225: addFocusListener(this );
0226: }
0227: } else {
0228: if (timer != null) {
0229: timer.stop();
0230: timer = null;
0231: removeFocusListener(this );
0232: setCaretVisible(true);
0233: }
0234: }
0235: }
0236:
0237: protected void finalize() throws Throwable {
0238: if (timer != null) {
0239: timer.stop();
0240: timer = null;
0241: }
0242: }
0243:
0244: private static final int getMinCharWidth(FontMetrics fm) {
0245: int minWidth = Integer.MAX_VALUE;
0246: int[] widths = fm.getWidths();
0247: int limit = widths.length > 0x7e ? 0x7e : widths.length;
0248: for (int i = limit; i >= 32; i--)
0249: if (widths[i] != 0 && widths[i] < minWidth)
0250: minWidth = widths[i];
0251: return minWidth;
0252: }
0253:
0254: public static final int getCharHeight() {
0255: return charHeight;
0256: }
0257:
0258: public static final int getCharWidth() {
0259: return charWidth;
0260: }
0261:
0262: public static final int getImageBorderHeight() {
0263: return 5;
0264: }
0265:
0266: public static final int getImageBorderWidth() {
0267: return 5;
0268: }
0269:
0270: public final Line getTopLine() {
0271: return topLine;
0272: }
0273:
0274: public final int getTopLineNumber() {
0275: return topLine.lineNumber();
0276: }
0277:
0278: public final void setTopLine(Line line) {
0279: topLine = line;
0280: pixelsAboveTopLine = 0;
0281: }
0282:
0283: public final int getPixelsAboveTopLine() {
0284: return pixelsAboveTopLine;
0285: }
0286:
0287: public final void setPixelsAboveTopLine(int pixels) {
0288: pixelsAboveTopLine = pixels;
0289: }
0290:
0291: public final int getShift() {
0292: return shift;
0293: }
0294:
0295: public final void setShift(int n) {
0296: this .shift = n;
0297: }
0298:
0299: public final int getCaretCol() {
0300: return caretCol;
0301: }
0302:
0303: public final void setCaretCol(int n) {
0304: caretCol = n;
0305: }
0306:
0307: public int getAbsoluteCaretCol() {
0308: return caretCol + shift;
0309: }
0310:
0311: public void setAbsoluteCaretCol(int col) {
0312: caretCol = col - shift;
0313: }
0314:
0315: public final void repaintNow() {
0316: paintImmediately(0, 0, getWidth(), getHeight());
0317: }
0318:
0319: public synchronized void repaintChangedLines() {
0320: if (!Editor.displayReady())
0321: return;
0322: if ((updateFlag & REPAINT) == REPAINT) {
0323: repaint();
0324: return;
0325: }
0326: if (changedLines.isEmpty())
0327: return;
0328: final Buffer buffer = editor.getBuffer();
0329: initializePaint();
0330: try {
0331: buffer.lockRead();
0332: } catch (InterruptedException e) {
0333: Log.error(e);
0334: return;
0335: }
0336: try {
0337: Graphics2D g2d = (Graphics2D) getGraphics();
0338: if (g2d != null) {
0339: Line line = topLine;
0340: int y = -pixelsAboveTopLine;
0341: final int limit = getHeight();
0342: while (line != null && y < limit) {
0343: if (changedLines.containsKey(line))
0344: paintLine(line, g2d, y);
0345: y += line.getHeight();
0346: line = line.nextVisible();
0347: }
0348: if (y < limit) {
0349: g2d.setColor(editor.getFormatter()
0350: .getBackgroundColor());
0351: final int height = limit - y;
0352: g2d.fillRect(0, y, getWidth(), height);
0353: if (showLineNumbers)
0354: drawGutterBorder(g2d, y, height);
0355: drawVerticalRule(g2d, y, height);
0356: }
0357: drawCaret(g2d);
0358: }
0359: } finally {
0360: buffer.unlockRead();
0361: }
0362: changedLines.clear();
0363: }
0364:
0365: // Set caret column to be where dot is.
0366: public void moveCaretToDotCol() {
0367: if (editor.getDot() == null)
0368: return;
0369: int absCol = editor.getDotCol();
0370: if (caretCol != absCol - shift) {
0371: caretCol = absCol - shift;
0372: lineChanged(editor.getDotLine());
0373: }
0374: setUpdateFlag(REFRAME);
0375: }
0376:
0377: // Assumes line is after topLine.
0378: private int getY(Line line) {
0379: int y = -pixelsAboveTopLine;
0380: int limit = getHeight();
0381: for (Line l = topLine; y < limit && l != null && l != line; l = l
0382: .nextVisible())
0383: y += l.getHeight();
0384: return y;
0385: }
0386:
0387: // Does NOT assume line is after topLine.
0388: private int getAbsoluteY(Line line) {
0389: int y = 0;
0390: for (Line l = editor.getBuffer().getFirstLine(); l != null
0391: && l != line; l = l.nextVisible())
0392: y += l.getHeight();
0393: return y;
0394: }
0395:
0396: private void initializePaint() {
0397: final Buffer buffer = editor.getBuffer();
0398: final Mode mode = editor.getMode();
0399: showChangeMarks = buffer
0400: .getBooleanProperty(Property.SHOW_CHANGE_MARKS);
0401: enableChangeMarks = showChangeMarks && !buffer.isNewFile();
0402: if (showChangeMarks) {
0403: changeColor = mode.getColorProperty(Property.COLOR_CHANGE);
0404: if (changeColor == null)
0405: changeColor = DefaultTheme.getColor("change");
0406: savedChangeColor = mode
0407: .getColorProperty(Property.COLOR_SAVED_CHANGE);
0408: if (savedChangeColor == null)
0409: savedChangeColor = DefaultTheme.getColor("savedChange");
0410: }
0411: showLineNumbers = buffer
0412: .getBooleanProperty(Property.SHOW_LINE_NUMBERS);
0413: gutterWidth = getGutterWidth(showChangeMarks, showLineNumbers);
0414: if (showLineNumbers) {
0415: lineNumberColor = mode
0416: .getColorProperty(Property.COLOR_LINE_NUMBER);
0417: if (lineNumberColor == null)
0418: lineNumberColor = DefaultTheme.getColor("lineNumber");
0419: gutterBorderColor = mode
0420: .getColorProperty(Property.COLOR_GUTTER_BORDER);
0421: if (gutterBorderColor == null)
0422: gutterBorderColor = DefaultTheme
0423: .getColor("gutterBorder");
0424: }
0425: int col = buffer.getIntegerProperty(Property.VERTICAL_RULE);
0426: if (col != 0) {
0427: verticalRuleX = gutterWidth + (col - shift) * charWidth - 1;
0428: verticalRuleColor = mode
0429: .getColorProperty(Property.COLOR_VERTICAL_RULE);
0430: if (verticalRuleColor == null)
0431: verticalRuleColor = DefaultTheme
0432: .getColor("verticalRule");
0433: } else
0434: verticalRuleX = 0;
0435: highlightBrackets = buffer
0436: .getBooleanProperty(Property.HIGHLIGHT_BRACKETS);
0437: highlightMatchingBracket = highlightBrackets
0438: || buffer
0439: .getBooleanProperty(Property.HIGHLIGHT_MATCHING_BRACKET);
0440:
0441: if (highlightMatchingBracket) {
0442: Position oldPosMatch = posMatch;
0443: posBracket = null;
0444: posMatch = null;
0445: if (editor.getDot() != null) {
0446: Position dot = editor.getDotCopy();
0447: char c = dot.getChar();
0448: if (c == '{' || c == '[' || c == '(') {
0449: posBracket = dot;
0450: posMatch = editor.findMatchInternal(dot, 200);
0451: } else if (dot.getOffset() > 0) {
0452: int end = editor.getBuffer().getCol(dot.getLine(),
0453: dot.getLine().length());
0454: if (shift + caretCol <= end) {
0455: dot.skip(-1);
0456: c = dot.getChar();
0457: if (c == '}' || c == ']' || c == ')') {
0458: posBracket = dot;
0459: posMatch = editor.findMatchInternal(dot,
0460: 200);
0461: }
0462: }
0463: }
0464: }
0465: if (oldPosMatch != null && oldPosMatch != posMatch)
0466: lineChanged(oldPosMatch.getLine());
0467: if (posMatch != null && posMatch != oldPosMatch)
0468: lineChanged(posMatch.getLine());
0469: if (!highlightBrackets)
0470: posBracket = null;
0471: }
0472: }
0473:
0474: private void drawVerticalRule(Graphics g, int y, int height) {
0475: if (verticalRuleX > gutterWidth) {
0476: g.setColor(verticalRuleColor);
0477: g.drawLine(verticalRuleX, y, verticalRuleX, y + height);
0478: }
0479: }
0480:
0481: private Position dragCaretPos;
0482:
0483: public void setDragCaretPos(Position pos) {
0484: if (dragCaretPos != null)
0485: lineChanged(dragCaretPos.getLine());
0486: dragCaretPos = pos;
0487: if (pos != null)
0488: lineChanged(pos.getLine());
0489: }
0490:
0491: private int dragCaretCol;
0492:
0493: public void setDragCaretCol(int col) {
0494: dragCaretCol = col;
0495: }
0496:
0497: // Called only from synchronized methods.
0498: private void drawDragCaret() {
0499: if (dragCaretPos == null)
0500: return;
0501: if (topLine == null)
0502: return;
0503: final Line line = dragCaretPos.getLine();
0504: if (line.lineNumber() < topLine.lineNumber())
0505: return;
0506: final int absCol;
0507: if (editor.getBuffer().getBooleanProperty(
0508: Property.RESTRICT_CARET))
0509: absCol = editor.getBuffer().getCol(dragCaretPos);
0510: else
0511: absCol = dragCaretCol; // We can go beyond the end of the line.
0512: if (absCol < shift)
0513: return;
0514: final int col = absCol - shift;
0515: formatLine(line, shift, col);
0516: Graphics2D g2d = (Graphics2D) getGraphics();
0517: final int x = gutterWidth
0518: + measureLine(g2d, textArray, col, formatArray);
0519: final int y = getY(line);
0520: g2d.setColor(editor.getFormatter().getCaretColor());
0521: g2d.fillRect(x, y, 1, charAscent + charDescent);
0522: }
0523:
0524: // Called only from synchronized methods.
0525: private void drawCaret(Graphics2D g2d) {
0526: if (dragCaretPos != null) {
0527: drawDragCaret();
0528: return;
0529: }
0530:
0531: if (!caretVisible)
0532: return;
0533: if (topLine == null)
0534: return;
0535: if (editor != Editor.currentEditor())
0536: return;
0537: if (editor.getDot() == null)
0538: return;
0539: if (editor.getMark() != null
0540: && !editor.getMark().equals(editor.getDot()))
0541: return;
0542: if (caretCol < 0)
0543: return;
0544: if (!editor.getFrame().isActive())
0545: return;
0546: if (editor.getFrame().getFocusedComponent() != this )
0547: return;
0548: final Line dotLine = editor.getDotLine();
0549: if (dotLine instanceof ImageLine)
0550: return;
0551: if (editor.getBuffer().needsRenumbering())
0552: editor.getBuffer().renumber();
0553: if (dotLine.lineNumber() < topLine.lineNumber())
0554: return;
0555:
0556: int x;
0557: if (caretCol == 0)
0558: x = gutterWidth;
0559: else if (dotLine.length() == 0)
0560: x = gutterWidth + caretCol * spaceWidth;
0561: else {
0562: formatLine(dotLine, shift, caretCol);
0563: x = gutterWidth
0564: + measureLine(g2d, textArray, caretCol, formatArray);
0565: }
0566:
0567: if (x > getWidth())
0568: return;
0569:
0570: int y = getY(dotLine);
0571: if (y >= getHeight())
0572: return;
0573:
0574: g2d.setColor(editor.getFormatter().getCaretColor());
0575:
0576: // Caret width is 1 pixel.
0577: g2d.fillRect(x, y, 1, charAscent + charDescent);
0578: }
0579:
0580: public synchronized void setCaretVisible(boolean b) {
0581: caretVisible = b;
0582: if (b && timer != null && timer.isRunning())
0583: timer.restart();
0584: }
0585:
0586: private synchronized void blinkCaret() {
0587: Position dot = editor.getDot();
0588: if (dot != null) {
0589: caretVisible = !caretVisible;
0590: final Line line = dot.getLine();
0591: Runnable r = new Runnable() {
0592: public void run() {
0593: repaintLine(line);
0594: }
0595: };
0596: SwingUtilities.invokeLater(r);
0597: }
0598: }
0599:
0600: private synchronized void repaintLine(Line l) {
0601: if (!Editor.displayReady())
0602: return;
0603: if ((updateFlag & REPAINT) == REPAINT) {
0604: repaint();
0605: return;
0606: }
0607: final Buffer buffer = editor.getBuffer();
0608: initializePaint();
0609: try {
0610: buffer.lockRead();
0611: } catch (InterruptedException e) {
0612: Log.error(e);
0613: return;
0614: }
0615: try {
0616: Graphics2D g2d = (Graphics2D) getGraphics();
0617: if (g2d != null) {
0618: Line line = topLine;
0619: int y = -pixelsAboveTopLine;
0620: final int limit = getHeight();
0621: while (line != null && y < limit) {
0622: if (line == l) {
0623: paintLine(line, g2d, y);
0624: break;
0625: }
0626: y += line.getHeight();
0627: line = line.nextVisible();
0628: }
0629: drawCaret(g2d);
0630: }
0631: } finally {
0632: buffer.unlockRead();
0633: }
0634: }
0635:
0636: // Timer event handler.
0637: public void actionPerformed(ActionEvent e) {
0638: blinkCaret();
0639: }
0640:
0641: public synchronized void focusGained(FocusEvent e) {
0642: if (timer != null)
0643: timer.start();
0644: }
0645:
0646: public synchronized void focusLost(FocusEvent e) {
0647: if (timer != null)
0648: timer.stop();
0649: }
0650:
0651: private int formatLine(final Line line, final int begin,
0652: final int maxCols) {
0653: // Avoid getfield overhead.
0654: final int[] fa = formatArray;
0655: final char[] ta = textArray;
0656: final int taLength = ta.length;
0657: Debug.assertTrue(taLength == fa.length);
0658: for (int i = taLength; i-- > 0;) {
0659: ta[i] = ' ';
0660: fa[i] = 0;
0661: }
0662: final int limit = Math.min(maxCols, taLength);
0663: final LineSegmentList segmentList = editor.getFormatter()
0664: .formatLine(line);
0665: int segmentStart = 0;
0666: int totalChars = 0;
0667: final int size = segmentList.size();
0668: for (int i = 0; i < size; i++) {
0669: final LineSegment segment = segmentList.getSegment(i);
0670: final int segmentLength = segment.length();
0671: if (segmentStart + segmentLength < begin) {
0672: segmentStart += segmentLength;
0673: continue;
0674: }
0675: final int maxAppend = limit - totalChars;
0676: if (segmentStart >= begin) {
0677: if (segmentLength <= maxAppend) {
0678: segment.getChars(0, segmentLength, ta, totalChars);
0679: totalChars += segmentLength;
0680: } else if (maxAppend > 0) {
0681: segment.getChars(0, maxAppend, ta, totalChars);
0682: totalChars += maxAppend;
0683: }
0684: } else {
0685: // segmentStart < begin && segmentStart + segmentLength >= begin
0686: String text = segment.substring(begin - segmentStart);
0687: if (text.length() <= maxAppend) {
0688: text.getChars(0, text.length(), ta, totalChars);
0689: totalChars += text.length();
0690: } else if (maxAppend > 0) {
0691: text.getChars(0, maxAppend, ta, totalChars);
0692: totalChars += maxAppend;
0693: }
0694: }
0695: final int format = segment.getFormat();
0696: int k = segmentStart - begin;
0697: if (k > limit)
0698: break;
0699: for (int j = 0; j < segmentLength; j++, k++) {
0700: if (k >= 0 && k < limit)
0701: fa[k] = format;
0702: }
0703: segmentStart += segmentLength;
0704: }
0705: return totalChars;
0706: }
0707:
0708: private Image paintLineImage;
0709: private int paintLineImageWidth;
0710: private int paintLineImageHeight;
0711: private Graphics2D paintLineGraphics;
0712:
0713: private final void providePaintLineImage(int width, int height) {
0714: if (paintLineImage != null && paintLineImageWidth == width
0715: && paintLineImageHeight == height)
0716: return;
0717:
0718: // Otherwise...
0719: paintLineImage = createImage(width, height);
0720: paintLineImageWidth = width;
0721: paintLineImageHeight = height;
0722: paintLineGraphics = (Graphics2D) paintLineImage.getGraphics();
0723:
0724: if (antialias) {
0725: paintLineGraphics.setRenderingHint(
0726: RenderingHints.KEY_TEXT_ANTIALIASING,
0727: RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
0728: }
0729: }
0730:
0731: private final void paintLine(Line line, Graphics2D g2d, int y) {
0732: if (line instanceof ImageLine)
0733: paintImageLine((ImageLine) line, g2d, y);
0734: else
0735: paintTextLine(line, g2d, y);
0736: }
0737:
0738: private synchronized void paintTextLine(Line line, Graphics g, int y) {
0739: int displayWidth = getWidth();
0740: int maxCols = getMaxCols();
0741:
0742: providePaintLineImage(displayWidth, charHeight);
0743:
0744: Color backgroundColor;
0745: if (line == getCurrentLine())
0746: backgroundColor = editor.getFormatter()
0747: .getCurrentLineBackgroundColor();
0748: else
0749: backgroundColor = editor.getFormatter()
0750: .getBackgroundColor();
0751: drawBackgroundForLine(paintLineGraphics, backgroundColor, line,
0752: 0);
0753:
0754: int totalChars = formatLine(line, shift, maxCols);
0755:
0756: if (editor.getMark() != null) {
0757: // Selection.
0758: Region r = new Region(editor);
0759: handleSelection(r, line, formatArray, paintLineGraphics, 0);
0760: } else if (posMatch != null) {
0761: if (posMatch.getLine() == line)
0762: highlightBracket(posMatch, line, formatArray,
0763: paintLineGraphics, 0);
0764: if (posBracket != null && posBracket.getLine() == line)
0765: highlightBracket(posBracket, line, formatArray,
0766: paintLineGraphics, 0);
0767: }
0768:
0769: drawGutterText(paintLineGraphics, line, 0);
0770: if (showLineNumbers && editor.getDot() != null)
0771: drawGutterBorder(paintLineGraphics, 0, line.getHeight());
0772: drawVerticalRule(paintLineGraphics, 0, line.getHeight());
0773: drawText(paintLineGraphics, textArray, totalChars, formatArray,
0774: 0);
0775: changedLines.remove(line);
0776:
0777: g.drawImage(paintLineImage, 0, y, null);
0778: }
0779:
0780: private void paintImageLine(ImageLine imageLine, Graphics g, int y) {
0781: final int displayWidth = getWidth();
0782: final int lineHeight = imageLine.getHeight();
0783: final int imageWidth = imageLine.getImageWidth();
0784: final int imageHeight = imageLine.getImageHeight();
0785: final int x = gutterWidth - shift * charWidth;
0786:
0787: Color backgroundColor;
0788: if (imageLine == getCurrentLine())
0789: backgroundColor = editor.getFormatter()
0790: .getCurrentLineBackgroundColor();
0791: else
0792: backgroundColor = editor.getFormatter()
0793: .getBackgroundColor();
0794:
0795: g.setColor(backgroundColor);
0796: // Left.
0797: g.fillRect(0, y, x, lineHeight);
0798: // Right.
0799: g.fillRect(x + imageWidth, y, displayWidth - (x + imageWidth),
0800: lineHeight);
0801: // Bottom.
0802: if (imageHeight < lineHeight)
0803: g.fillRect(0, y + imageHeight, displayWidth, lineHeight
0804: - imageHeight);
0805:
0806: Rectangle rect = imageLine.getRect();
0807: g.drawImage(imageLine.getImage(), x, y, x + rect.width, y
0808: + rect.height, rect.x, rect.y, rect.x + rect.width,
0809: rect.y + rect.height, null);
0810: }
0811:
0812: private void drawBackgroundForLine(Graphics2D g2d,
0813: Color backgroundColor, Line line, int y) {
0814: if (enableChangeMarks && line.isModified()) {
0815: g2d.setColor(line.isSaved() ? savedChangeColor
0816: : changeColor);
0817: g2d.fillRect(0, y, changeMarkWidth, line.getHeight());
0818: g2d.setColor(backgroundColor);
0819: g2d.fillRect(changeMarkWidth, y, getWidth()
0820: - changeMarkWidth, line.getHeight());
0821: } else {
0822: g2d.setColor(backgroundColor);
0823: g2d.fillRect(0, y, getWidth(), line.getHeight());
0824: }
0825: }
0826:
0827: private void drawGutterText(Graphics g, Line line, int y) {
0828: int x = showChangeMarks ? changeMarkWidth : 0;
0829: char c = 0;
0830: Annotation annotation = line.getAnnotation();
0831: if (annotation != null)
0832: c = annotation.getGutterChar();
0833: else if (line.next() != null && line.next().isHidden())
0834: c = '+';
0835: if (c != 0) {
0836: char[] chars = new char[1];
0837: chars[0] = c;
0838: g.setColor(editor.getFormatter().getColor(0)); // Default text color.
0839: g.setFont(plainFont);
0840: g.drawChars(chars, 0, 1, x, y + charAscent);
0841: }
0842: x += charWidth;
0843: if (showLineNumbers) {
0844: final String s = String.valueOf(line.lineNumber() + 1);
0845: final int pad = MAX_LINE_NUMBER_CHARS - s.length();
0846: if (pad >= 0) {
0847: x += pad * gutterCharWidth;
0848: g.setColor(lineNumberColor);
0849: g.setFont(gutterFont);
0850: g.drawString(s, x, y + charAscent);
0851: }
0852: }
0853: }
0854:
0855: private void drawGutterBorder(Graphics g) {
0856: int x = getGutterWidth(editor.getBuffer()) - 4;
0857: g.setColor(gutterBorderColor);
0858: g.drawLine(x, 0, x, getHeight());
0859: }
0860:
0861: private void drawGutterBorder(Graphics g, int y, int height) {
0862: int x = getGutterWidth(editor.getBuffer()) - 4;
0863: g.setColor(gutterBorderColor);
0864: g.drawLine(x, y, x, y + height);
0865: }
0866:
0867: // Returns width in pixels.
0868: public static final int getGutterWidth(Buffer buffer) {
0869: return getGutterWidth(buffer
0870: .getBooleanProperty(Property.SHOW_CHANGE_MARKS), buffer
0871: .getBooleanProperty(Property.SHOW_LINE_NUMBERS));
0872: }
0873:
0874: // Returns width in pixels.
0875: private static final int getGutterWidth(boolean showChangeMarks,
0876: boolean showLineNumbers) {
0877: int width = charWidth;
0878: if (showChangeMarks)
0879: width += changeMarkWidth;
0880: if (showLineNumbers)
0881: width += MAX_LINE_NUMBER_CHARS * gutterCharWidth + 5;
0882: return width;
0883: }
0884:
0885: private void drawText(Graphics2D g2d, char[] textArray, int length,
0886: int[] formatArray, int y) {
0887: int i = 0;
0888: double x = gutterWidth;
0889: final Formatter formatter = editor.getFormatter();
0890: while (i < length) {
0891: int format = formatArray[i];
0892: int start = i;
0893: while (formatArray[i] == format && i < length)
0894: ++i;
0895: int style;
0896: FormatTableEntry entry = formatter
0897: .getFormatTableEntry(format);
0898: if (entry != null) {
0899: g2d.setColor(entry.getColor());
0900: style = entry.getStyle();
0901: } else {
0902: // Web mode.
0903: g2d.setColor(formatter.getColor(format));
0904: style = formatter.getStyle(format);
0905: }
0906: Font font;
0907: switch (style) {
0908: case Font.BOLD:
0909: font = boldFont;
0910: break;
0911: case Font.ITALIC:
0912: font = italicFont;
0913: break;
0914: case Font.PLAIN:
0915: default:
0916: font = plainFont;
0917: break;
0918: }
0919: char[] chars = new char[i - start];
0920: System.arraycopy(textArray, start, chars, 0, i - start);
0921: GlyphVector gv = font.createGlyphVector(g2d
0922: .getFontRenderContext(), chars);
0923: final double width = gv.getLogicalBounds().getWidth();
0924: if (style == Font.BOLD) {
0925: if (boldFont == plainFont) {
0926: if (underlineBold)
0927: g2d.drawLine((int) x, y + charAscent + 1,
0928: (int) (x + width), y + charAscent + 1);
0929: else
0930: g2d.drawGlyphVector(gv, (int) x + 1, y
0931: + charAscent);
0932: } else if (emulateBold)
0933: g2d.drawGlyphVector(gv, (float) x + 1, y
0934: + charAscent);
0935: }
0936: if (formatter.getUnderline(format))
0937: g2d.drawLine((int) x, y + charAscent + 1,
0938: (int) (x + width), y + charAscent + 1);
0939: g2d.drawGlyphVector(gv, (float) x, y + charAscent);
0940: x += width;
0941: }
0942: }
0943:
0944: private int measureLine(Graphics2D g2d, char[] textArray,
0945: int length, int[] formatArray) {
0946: if (length == 0)
0947: return 0;
0948: final int limit = Math.min(length, textArray.length);
0949: double totalWidth = 0;
0950: int i = 0;
0951: Formatter formatter = editor.getFormatter();
0952: while (i < limit) {
0953: int format = formatArray[i];
0954: int startCol = i;
0955: while (i < limit && formatArray[i] == format)
0956: ++i;
0957: Font font;
0958: switch (formatter.getStyle(format)) {
0959: case Font.BOLD:
0960: font = boldFont;
0961: break;
0962: case Font.ITALIC:
0963: font = italicFont;
0964: break;
0965: case Font.PLAIN:
0966: default:
0967: font = plainFont;
0968: break;
0969: }
0970: char[] chars = new char[i - startCol];
0971: System.arraycopy(textArray, startCol, chars, 0, i
0972: - startCol);
0973: GlyphVector gv = font.createGlyphVector(g2d
0974: .getFontRenderContext(), chars);
0975: totalWidth += gv.getLogicalBounds().getWidth();
0976: }
0977: return (int) totalWidth;
0978: }
0979:
0980: public void paintComponent(Graphics g) {
0981: final Buffer buffer = editor.getBuffer();
0982: if (!Editor.displayReady()) {
0983: if (buffer != null && buffer.getModeId() == IMAGE_MODE)
0984: g.setColor(ImageBuffer.getDefaultBackgroundColor());
0985: else
0986: g.setColor(editor.getFormatter().getBackgroundColor());
0987: g.fillRect(0, 0, getWidth(), getHeight());
0988: return;
0989: }
0990: try {
0991: buffer.lockRead();
0992: } catch (InterruptedException e) {
0993: Log.error(e);
0994: return;
0995: }
0996: try {
0997: if (buffer.getModeId() == IMAGE_MODE)
0998: paintImage(g);
0999: else
1000: paintComponentInternal(g);
1001: } finally {
1002: buffer.unlockRead();
1003: }
1004: }
1005:
1006: private void paintImage(Graphics g) {
1007: ImageBuffer ib = (ImageBuffer) editor.getBuffer();
1008: g.setColor(ib.getBackgroundColor());
1009: g.fillRect(0, 0, getWidth(), getHeight());
1010: Image image = ib.getImage();
1011: if (image != null) {
1012: int imageWidth = image.getWidth(null);
1013: int imageHeight = image.getHeight(null);
1014: int x = 0;
1015: int y = 0;
1016: if (imageWidth > 0 && imageHeight > 0) {
1017: if (imageWidth < getWidth())
1018: x = (getWidth() - imageWidth) / 2;
1019: if (imageHeight < getHeight())
1020: y = (getHeight() - imageHeight) / 2;
1021: }
1022: if (x < getImageBorderWidth())
1023: x = getImageBorderWidth();
1024: if (y < getImageBorderHeight())
1025: y = getImageBorderHeight();
1026: g.drawImage(image, x - shift * charWidth, y
1027: - pixelsAboveTopLine, this );
1028: }
1029: }
1030:
1031: private synchronized void paintComponentInternal(Graphics g) {
1032: initializePaint();
1033: Graphics2D g2d = (Graphics2D) g;
1034: if (antialias) {
1035: g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING,
1036: RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
1037: }
1038: final Rectangle clipBounds = g2d.getClipBounds();
1039: final int displayWidth = getWidth();
1040: final int maxCols = getMaxCols();
1041:
1042: // Selection.
1043: final Region r = editor.getMark() != null ? new Region(editor)
1044: : null;
1045:
1046: // Current line.
1047: final Line currentLine = getCurrentLine();
1048:
1049: final Color colorBackground = editor.getFormatter()
1050: .getBackgroundColor();
1051: int y = -pixelsAboveTopLine;
1052: Line line = topLine;
1053: while (line != null && y + line.getHeight() < clipBounds.y) {
1054: y += line.getHeight();
1055: line = line.nextVisible();
1056: }
1057: final int limit = clipBounds.y + clipBounds.height;
1058: while (line != null && y < limit) {
1059: if (line instanceof ImageLine) {
1060: paintImageLine((ImageLine) line, g2d, y);
1061: } else {
1062: Color backgroundColor;
1063: if (line == currentLine) {
1064: backgroundColor = editor.getFormatter()
1065: .getCurrentLineBackgroundColor();
1066: } else
1067: backgroundColor = colorBackground;
1068: drawBackgroundForLine(g2d, backgroundColor, line, y);
1069: int totalChars = formatLine(line, shift, maxCols);
1070: if (r != null)
1071: handleSelection(r, line, formatArray, g2d, y);
1072: else if (posMatch != null) {
1073: if (posMatch.getLine() == line)
1074: highlightBracket(posMatch, line, formatArray,
1075: g2d, y);
1076: if (posBracket != null
1077: && posBracket.getLine() == line)
1078: highlightBracket(posBracket, line, formatArray,
1079: g2d, y);
1080: }
1081: drawGutterText(g2d, line, y);
1082: if (totalChars > 0) {
1083: // Draw vertical rule first so it will be behind the text.
1084: drawVerticalRule(g2d, y, line.getHeight());
1085: drawText(g2d, textArray, totalChars, formatArray, y);
1086: } else
1087: drawVerticalRule(g2d, y, line.getHeight());
1088: changedLines.remove(line);
1089: }
1090: y += line.getHeight();
1091: line = line.nextVisible();
1092: }
1093: if (y < limit) {
1094: g2d.setColor(colorBackground);
1095: g2d.fillRect(0, y, displayWidth, limit - y);
1096: drawVerticalRule(g2d, y, limit - y);
1097: }
1098: drawCaret(g2d);
1099: if (showLineNumbers && editor.getDot() != null)
1100: drawGutterBorder(g2d);
1101: updateFlag &= ~REPAINT;
1102: }
1103:
1104: private Line getCurrentLine() {
1105: if (editor.getDot() != null && editor.getMark() == null)
1106: return editor.getDotLine();
1107: return null;
1108: }
1109:
1110: private void handleSelection(Region r, Line line,
1111: int[] formatArray, Graphics2D g2d, int y) {
1112: if (r == null)
1113: return;
1114:
1115: int maxCols = getMaxCols();
1116: int fillHeight = charHeight;
1117: int fillWidth = 0;
1118: int beginCol = 0;
1119: int endCol = 0;
1120: int x = 0;
1121:
1122: if (r.isColumnRegion()) {
1123: if (line.lineNumber() >= r.getBeginLineNumber()
1124: && line.lineNumber() <= r.getEndLineNumber()) {
1125: beginCol = r.getBeginCol() - shift;
1126: endCol = r.getEndCol() - shift;
1127:
1128: if (beginCol < 0)
1129: beginCol = 0;
1130: if (endCol < 0)
1131: endCol = 0;
1132: if (endCol > maxCols)
1133: endCol = maxCols;
1134:
1135: int x1 = measureLine(g2d, textArray, beginCol,
1136: formatArray);
1137: int x2 = measureLine(g2d, textArray, endCol,
1138: formatArray);
1139: fillWidth = x2 - x1;
1140: x = gutterWidth + x1;
1141: }
1142: } else if (line == r.getBeginLine()) {
1143: beginCol = r.getBeginCol() - shift;
1144: if (line == r.getEndLine())
1145: endCol = r.getEndCol() - shift;
1146:
1147: if (beginCol < 0)
1148: beginCol = 0;
1149: if (endCol < 0)
1150: endCol = 0;
1151: if (endCol > maxCols)
1152: endCol = maxCols;
1153:
1154: if (line == r.getEndLine()) {
1155: int x1 = measureLine(g2d, textArray, beginCol,
1156: formatArray);
1157: int x2 = measureLine(g2d, textArray, endCol,
1158: formatArray);
1159: fillWidth = x2 - x1;
1160: x = gutterWidth + x1;
1161: } else {
1162: fillWidth = getWidth();
1163: x = gutterWidth
1164: + measureLine(g2d, textArray, beginCol,
1165: formatArray);
1166: }
1167: } else if (line.lineNumber() > r.getBeginLineNumber()
1168: && line.lineNumber() < r.getEndLineNumber()) {
1169: // Entire line is selected.
1170: fillWidth = getWidth();
1171: x = gutterWidth;
1172: } else if (line == r.getEndLine()) {
1173: // Last line of selection that spans more than one line.
1174: endCol = r.getEndCol() - shift;
1175:
1176: if (endCol < 0)
1177: endCol = 0;
1178: if (endCol > maxCols)
1179: endCol = maxCols;
1180:
1181: int x1 = measureLine(g2d, textArray, beginCol, formatArray);
1182: int x2 = measureLine(g2d, textArray, endCol, formatArray);
1183: fillWidth = x2 - x1;
1184: x = gutterWidth + x1;
1185: }
1186:
1187: if (fillWidth > 0) {
1188: g2d.setColor(editor.getFormatter()
1189: .getSelectionBackgroundColor());
1190: g2d.fillRect(x, y, fillWidth, charHeight);
1191: }
1192: }
1193:
1194: private void highlightBracket(Position pos, Line line,
1195: int[] formatArray, Graphics2D g2d, int y) {
1196: if (pos == null) {
1197: Debug.bug();
1198: return;
1199: }
1200: if (pos.getLine() != line) {
1201: Debug.bug();
1202: return;
1203: }
1204: if (editor.getFrame().getFocusedComponent() != this )
1205: return;
1206: int beginCol = editor.getBuffer().getCol(pos) - shift;
1207: if (beginCol < 0)
1208: return;
1209: int endCol = beginCol + 1;
1210: int x1 = measureLine(g2d, textArray, beginCol, formatArray);
1211: int x2 = measureLine(g2d, textArray, endCol, formatArray);
1212: int fillWidth = x2 - x1;
1213: int x = gutterWidth + x1;
1214: if (fillWidth > 0) {
1215: g2d.setColor(editor.getFormatter()
1216: .getMatchingBracketBackgroundColor());
1217: g2d.fillRect(x, y, fillWidth, charHeight);
1218: }
1219: }
1220:
1221: // Scroll up in the buffer, moving the content in the window down.
1222: private void scrollUp() {
1223: if (editor.getModeId() == IMAGE_MODE) {
1224: if (pixelsAboveTopLine >= charHeight) {
1225: pixelsAboveTopLine -= charHeight;
1226: repaint();
1227: }
1228: return;
1229: }
1230:
1231: if (topLine != null) {
1232: if (topLine instanceof ImageLine) {
1233: if (pixelsAboveTopLine - charHeight >= 0) {
1234: pixelsAboveTopLine -= charHeight;
1235: scrollPixelsUp(charHeight);
1236: Rectangle r = new Rectangle(0, 0, getWidth(),
1237: charHeight);
1238: paintImmediately(r);
1239: return;
1240: }
1241: }
1242: Line line = topLine.previousVisible();
1243: if (line == null)
1244: return;
1245: if (line instanceof ImageLine) {
1246: scrollPixelsUp(charHeight);
1247: topLine = line;
1248: pixelsAboveTopLine = line.getHeight() - charHeight;
1249: editor.update(topLine);
1250: return;
1251: }
1252: scrollPixelsUp(charHeight);
1253: setTopLine(line);
1254: editor.update(topLine);
1255: }
1256: }
1257:
1258: // Scroll down in the buffer, moving the content in the window up.
1259: private void scrollDown() {
1260: if (editor.getModeId() == IMAGE_MODE) {
1261: pixelsAboveTopLine += charHeight;
1262: repaint();
1263: return;
1264: }
1265: if (topLine != null) {
1266: if (topLine instanceof ImageLine) {
1267: if (pixelsAboveTopLine + charHeight < topLine
1268: .getHeight()) {
1269: pixelsAboveTopLine += charHeight;
1270: scrollPixelsDown(charHeight);
1271: Rectangle r = new Rectangle();
1272: r.x = 0;
1273: r.y = getHeight() - charHeight;
1274: r.width = getWidth();
1275: r.height = charHeight;
1276: paintImmediately(r);
1277: return;
1278: }
1279: }
1280: Line line = topLine.nextVisible();
1281: if (line != null) {
1282: scrollPixelsDown(charHeight);
1283: setTopLine(line);
1284: Line bottomLine = getBottomLine();
1285: editor.update(bottomLine);
1286: Line nextVisible = bottomLine.nextVisible();
1287: if (nextVisible != null)
1288: editor.update(nextVisible);
1289: }
1290: }
1291: }
1292:
1293: // Move content down.
1294: private void scrollPixelsUp(int dy) {
1295: Point pt1 = editor.getFrame().getLocationOnScreen();
1296: Point pt2 = getLocationOnScreen();
1297: int x = pt2.x - pt1.x;
1298: int y = pt2.y - pt1.y;
1299: editor.getFrame().getGraphics().copyArea(x, y, getWidth(),
1300: getHeight() - dy, 0, dy);
1301: }
1302:
1303: // Move content up.
1304: private void scrollPixelsDown(int dy) {
1305: Point pt1 = editor.getFrame().getLocationOnScreen();
1306: Point pt2 = getLocationOnScreen();
1307: int x = pt2.x - pt1.x;
1308: int y = pt2.y - pt1.y + dy;
1309: editor.getFrame().getGraphics().copyArea(x, y, getWidth(),
1310: getHeight() - dy, 0, -dy);
1311: }
1312:
1313: public Line getBottomLine() {
1314: Line line = topLine;
1315: int y = line.getHeight() - pixelsAboveTopLine;
1316: final int limit = getHeight();
1317: while (true) {
1318: Line next = line.nextVisible();
1319: if (next == null)
1320: break;
1321: y += next.getHeight();
1322: if (y > limit)
1323: break;
1324: line = next;
1325: }
1326: return line;
1327: }
1328:
1329: public void up(boolean select) {
1330: if (editor.getDot() == null)
1331: return;
1332:
1333: if (select) {
1334: if (editor.getMark() == null)
1335: editor.addUndo(SimpleEdit.MOVE);
1336: else if (editor.getLastCommand() != COMMAND_UP)
1337: editor.addUndo(SimpleEdit.MOVE);
1338: } else {
1339: if (editor.getMark() != null) {
1340: boolean isLineBlock = (editor.getDotOffset() == 0 && editor
1341: .getMarkOffset() == 0);
1342: editor.addUndo(SimpleEdit.MOVE);
1343: editor.beginningOfBlock();
1344: editor.setGoalColumn(editor.getDotCol());
1345: if (isLineBlock)
1346: return;
1347: } else if (editor.getLastCommand() != COMMAND_UP)
1348: editor.addUndo(SimpleEdit.MOVE);
1349: }
1350:
1351: Line dotLine = editor.getDotLine();
1352: Line prevLine = dotLine.previousVisible();
1353: if (prevLine == null)
1354: return;
1355: if (dotLine == topLine) {
1356: // Need to scroll.
1357: windowUp();
1358: }
1359: editor.updateDotLine();
1360: final Buffer buffer = editor.getBuffer();
1361: boolean selectLine = false;
1362: if (select && editor.getMark() == null) {
1363: Position savedDot = null;
1364: if (buffer.getBooleanProperty(Property.AUTO_SELECT_LINE)) {
1365: Line nextLine = editor.getDotLine().next();
1366: if (nextLine != null) {
1367: selectLine = true;
1368: savedDot = new Position(editor.getDot());
1369: editor.getDot().moveTo(nextLine, 0);
1370: caretCol = 0;
1371: }
1372: }
1373: if (selectLine) {
1374: // Make sure absMarkCol will be correct.
1375: int savedShift = shift;
1376: shift = 0;
1377: editor.setMarkAtDot();
1378: shift = savedShift;
1379: } else
1380: editor.setMarkAtDot();
1381: if (savedDot != null)
1382: editor.getSelection().setSavedDot(savedDot);
1383: }
1384: editor.getDot().setLine(prevLine);
1385: editor.updateDotLine();
1386: if (selectLine)
1387: editor.setGoalColumn(0);
1388: editor.moveDotToGoalCol();
1389: }
1390:
1391: public void down(boolean select) {
1392: if (editor.getDot() == null)
1393: return;
1394: if (select) {
1395: if (editor.getMark() == null)
1396: editor.addUndo(SimpleEdit.MOVE);
1397: else if (editor.getLastCommand() != COMMAND_DOWN)
1398: editor.addUndo(SimpleEdit.MOVE);
1399: } else {
1400: if (editor.getMark() != null) {
1401: boolean isLineBlock = (editor.getDotOffset() == 0 && editor
1402: .getMarkOffset() == 0);
1403: editor.addUndo(SimpleEdit.MOVE);
1404: editor.endOfBlock();
1405: editor.setGoalColumn(editor.getDotCol());
1406: if (isLineBlock)
1407: return;
1408: } else if (editor.getLastCommand() != COMMAND_DOWN)
1409: editor.addUndo(SimpleEdit.MOVE);
1410: }
1411: final Line dotLine = editor.getDotLine();
1412: final Line nextLine = dotLine.nextVisible();
1413: if (nextLine == null)
1414: return;
1415: if (getY(nextLine) + nextLine.getHeight() > getHeight()) {
1416: // Need to scroll.
1417: windowDown();
1418: }
1419: editor.updateDotLine();
1420: final Buffer buffer = editor.getBuffer();
1421: boolean selectLine = false;
1422: if (select && editor.getMark() == null) {
1423: Position savedDot = null;
1424: if (buffer.getBooleanProperty(Property.AUTO_SELECT_LINE)) {
1425: selectLine = true;
1426: savedDot = new Position(editor.getDot());
1427: editor.getDot().setOffset(0);
1428: caretCol = 0;
1429: }
1430: if (selectLine) {
1431: // Make sure absMarkCol will be correct.
1432: int savedShift = shift;
1433: shift = 0;
1434: editor.setMarkAtDot();
1435: shift = savedShift;
1436: } else
1437: editor.setMarkAtDot();
1438: if (savedDot != null)
1439: editor.getSelection().setSavedDot(savedDot);
1440: }
1441: editor.getDot().setLine(nextLine);
1442: editor.updateDotLine();
1443: if (selectLine)
1444: editor.setGoalColumn(0);
1445: editor.moveDotToGoalCol();
1446: }
1447:
1448: public void windowUp() {
1449: if (getHeight() < editor.getBuffer().getDisplayHeight())
1450: scrollUp();
1451: }
1452:
1453: public void windowDown() {
1454: final int totalHeight = editor.getBuffer().getDisplayHeight();
1455: final int windowHeight = getHeight();
1456: if (windowHeight < totalHeight) {
1457: // Add up cumulative height to bottom of window.
1458: int y;
1459: if (topLine != null)
1460: y = editor.getBuffer().getY(topLine)
1461: + pixelsAboveTopLine + windowHeight;
1462: else
1463: y = pixelsAboveTopLine + windowHeight;
1464: if (y < totalHeight)
1465: scrollDown();
1466: }
1467: }
1468:
1469: public void windowUp(int lines) {
1470: Line line = topLine;
1471: if (line == null) {
1472: if (editor.getModeId() == IMAGE_MODE) {
1473: pixelsAboveTopLine -= lines * charHeight;
1474: if (pixelsAboveTopLine < 0)
1475: pixelsAboveTopLine = 0;
1476: repaint();
1477: }
1478: return;
1479: }
1480: if (line instanceof ImageLine) {
1481: imageLineWindowUp(lines);
1482: return;
1483: }
1484: int actual = 0;
1485: for (int i = 0; i < lines; i++) {
1486: Line prev = line.previousVisible();
1487: if (prev == null)
1488: break;
1489: if (prev instanceof ImageLine) {
1490: imageLineWindowUp(lines);
1491: return;
1492: }
1493: line = prev;
1494: lineChanged(line);
1495: ++actual;
1496: }
1497: scrollPixelsUp(actual * charHeight);
1498: setTopLine(line);
1499: editor.maybeScrollCaret();
1500: editor.updateDisplay();
1501: }
1502:
1503: private void imageLineWindowUp(int lines) {
1504: int oldY = getAbsoluteY(topLine) + pixelsAboveTopLine;
1505: int newY = oldY - lines * charHeight;
1506: if (newY < 0)
1507: newY = 0;
1508: Line line = lineFromAbsoluteY(newY);
1509: if (line != null) {
1510: int y = getAbsoluteY(line);
1511: topLine = line;
1512: pixelsAboveTopLine = newY - y;
1513: setUpdateFlag(REPAINT);
1514: editor.updateDisplay();
1515: }
1516: }
1517:
1518: public void windowDown(final int lines) {
1519: Line top = topLine;
1520: if (top == null) {
1521: if (editor.getModeId() == IMAGE_MODE) {
1522: int windowHeight = getHeight();
1523: int bufferHeight = editor.getBuffer()
1524: .getDisplayHeight();
1525: pixelsAboveTopLine += lines * charHeight;
1526: if (pixelsAboveTopLine + windowHeight > bufferHeight)
1527: pixelsAboveTopLine = bufferHeight - windowHeight;
1528: repaint();
1529: }
1530: return;
1531: }
1532: if (top instanceof ImageLine) {
1533: imageLineWindowDown(lines);
1534: return;
1535: }
1536: int actual = 0;
1537: Line bottom = getBottomLine();
1538: for (int i = 0; i < lines; i++) {
1539: bottom = bottom.nextVisible();
1540: if (bottom == null)
1541: break;
1542: lineChanged(bottom);
1543: Line next = top.nextVisible();
1544: if (next instanceof ImageLine) {
1545: imageLineWindowDown(lines);
1546: return;
1547: }
1548: if (next == null)
1549: break;
1550: top = next;
1551: ++actual;
1552: }
1553: if (bottom != null) {
1554: bottom = bottom.nextVisible();
1555: if (bottom != null)
1556: lineChanged(bottom);
1557: }
1558: scrollPixelsDown(actual * charHeight);
1559: setTopLine(top);
1560: editor.maybeScrollCaret();
1561: editor.updateDisplay();
1562: }
1563:
1564: private void imageLineWindowDown(int lines) {
1565: Line top = topLine;
1566: int oldY = getAbsoluteY(top) + pixelsAboveTopLine;
1567: int newY = oldY + lines * charHeight;
1568: int windowHeight = getHeight();
1569: int bufferHeight = editor.getBuffer().getDisplayHeight();
1570: if (newY + windowHeight > bufferHeight)
1571: newY = bufferHeight - windowHeight;
1572: if (newY == oldY)
1573: return;
1574: Line line = lineFromAbsoluteY(newY);
1575: if (line != null) {
1576: int y = getAbsoluteY(line);
1577: topLine = line;
1578: pixelsAboveTopLine = newY - y;
1579: setUpdateFlag(REPAINT);
1580: editor.updateDisplay();
1581: }
1582: }
1583:
1584: public void setUpdateFlag(int mask) {
1585: updateFlag |= mask;
1586: }
1587:
1588: private int reframeParam = 0;
1589:
1590: public void setReframe(int n) {
1591: reframeParam = n;
1592: }
1593:
1594: public void reframe() {
1595: if (!Editor.displayReady())
1596: return;
1597: if (editor.getDot() == null)
1598: return;
1599: if (getHeight() == 0)
1600: return; // Not visible yet.
1601: if (topLine == null || (updateFlag & REFRAME) != 0) {
1602: final Buffer buffer = editor.getBuffer();
1603: try {
1604: buffer.lockRead();
1605: } catch (InterruptedException e) {
1606: Log.error(e);
1607: return;
1608: }
1609: try {
1610: reframeHorizontally();
1611: reframeVertically();
1612: } finally {
1613: buffer.unlockRead();
1614: }
1615: updateFlag &= ~REFRAME;
1616: }
1617: }
1618:
1619: private void reframeVertically() {
1620: if (topLine != null && topLine.isHidden()) {
1621: Line prev = topLine.previousVisible();
1622: setTopLine(prev != null ? prev : topLine.nextVisible());
1623: setUpdateFlag(REPAINT);
1624: }
1625:
1626: if (topLine == null || mustReframe()) {
1627: Line top = findNewTopLine(editor.getDotLine());
1628: setTopLine(top);
1629: setUpdateFlag(REPAINT);
1630: }
1631:
1632: reframeParam = 0;
1633:
1634: // Now we need to check to make sure there's not unnecessary
1635: // whitespace at the bottom of the display.
1636:
1637: // If we can't go back any further, we have no choice.
1638: if (topLine.previousVisible() == null)
1639: return;
1640:
1641: int y = getAbsoluteY(topLine);
1642: int limit = editor.getBuffer().getDisplayHeight() - getHeight()
1643: + charHeight;
1644: if (y > limit) {
1645: // We need to scroll back in the buffer a bit.
1646: Line top = lineFromAbsoluteY(limit);
1647: setTopLine(top);
1648: setUpdateFlag(REPAINT);
1649: reframeParam = 0;
1650: }
1651: }
1652:
1653: // Returns true if necessary to reframe vertically.
1654: private boolean mustReframe() {
1655: final int height = getHeight();
1656: final Line dotLine = editor.getDotLine();
1657: Line line = topLine;
1658: int y = -pixelsAboveTopLine;
1659: while (y < height) {
1660: if (line == dotLine) {
1661: // Whole line must fit.
1662: return y + line.getHeight() > height;
1663: }
1664: Line next = line.nextVisible();
1665: if (next == null)
1666: return true;
1667: y += line.getHeight();
1668: line = next;
1669: }
1670: return true;
1671: }
1672:
1673: // Helper for reframeVertically().
1674: private Line findNewTopLine(final Line dotLine) {
1675: int y;
1676: if (reframeParam == 0)
1677: y = getHeight() / 2; // Default.
1678: else if (reframeParam > 0)
1679: y = (reframeParam - 1) * charHeight;
1680: else
1681: // reframeParam < 0
1682: y = getHeight() + reframeParam * charHeight;
1683:
1684: Line line = dotLine;
1685: while (true) {
1686: Line prev = line.previousVisible();
1687: if (prev == null)
1688: break;
1689: y -= prev.getHeight();
1690: if (y < 0)
1691: break;
1692: line = prev;
1693: }
1694:
1695: return line;
1696: }
1697:
1698: private void reframeHorizontally() {
1699: if (editor.getDot() == null)
1700: return;
1701: if (editor.getDotLine() instanceof ImageLine)
1702: return;
1703: final int absCaretCol = caretCol + shift;
1704: Debug.assertTrue(absCaretCol >= 0);
1705: ensureColumnVisible(editor.getDotLine(), absCaretCol);
1706: caretCol = absCaretCol - shift;
1707: }
1708:
1709: public synchronized void ensureColumnVisible(Line line, int absCol) {
1710: final int oldShift = shift;
1711: if (absCol < 50)
1712: shift = 0;
1713: int col = absCol - shift;
1714: if (col < 0) {
1715: do {
1716: shift -= 8;
1717: if (shift < 0)
1718: shift = 0;
1719: col = absCol - shift;
1720: } while (col < 0);
1721: } else {
1722: if (col > getMaxCols()) {
1723: shift = absCol - getMaxCols();
1724: col = absCol - shift;
1725: Debug.assertTrue(col == getMaxCols());
1726: }
1727: Graphics2D g2d = (Graphics2D) getGraphics();
1728: if (g2d == null) {
1729: Log.error("ensureColumnVisible g2d is null");
1730: return;
1731: }
1732: formatLine(line, shift, col);
1733: int x = measureLine(g2d, textArray, col, formatArray);
1734: final int maxWidth = getWidth() - gutterWidth - charWidth;
1735: while (x > maxWidth) {
1736: shift += 8;
1737: col = absCol - shift;
1738: formatLine(line, shift, col);
1739: x = measureLine(g2d, textArray, col, formatArray);
1740: }
1741: }
1742: if (shift != oldShift)
1743: setUpdateFlag(REPAINT);
1744: }
1745:
1746: public void toCenter() {
1747: Line line = editor.getDotLine();
1748: int limit = getRows() / 2;
1749: for (int i = 0; i < limit; i++) {
1750: Line prev = line.previousVisible();
1751: if (prev == null)
1752: break;
1753: line = prev;
1754: }
1755: setTopLine(line);
1756: setUpdateFlag(REPAINT);
1757: }
1758:
1759: public void toTop() {
1760: Line goal = editor.getDotLine().previousVisible();
1761: if (goal == null)
1762: goal = editor.getDotLine();
1763: if (topLine != goal) {
1764: setTopLine(goal);
1765: setUpdateFlag(REPAINT);
1766: }
1767: }
1768:
1769: // Does nothing if entire region is already visible.
1770: public void centerRegion(Line begin, Line end) {
1771: if (begin == null)
1772: return;
1773: if (end != null) {
1774: if (isLineVisible(begin) && isLineVisible(end))
1775: return; // Entire region is already visible.
1776: }
1777: Line newTopLine = null;
1778: int linesInRegion = 0;
1779: if (end != null) {
1780: for (Line line = begin; line != null && line.isBefore(end); line = line
1781: .nextVisible())
1782: ++linesInRegion;
1783: } else {
1784: for (Line line = begin; line != null; line = line
1785: .nextVisible())
1786: ++linesInRegion;
1787: }
1788: int numRows = getRows();
1789: if (numRows > linesInRegion) {
1790: int linesAbove = (numRows - linesInRegion) / 2;
1791: newTopLine = begin;
1792: do {
1793: Line prev = newTopLine.previousVisible();
1794: if (prev != null)
1795: newTopLine = prev;
1796: else
1797: break;
1798: --linesAbove;
1799: } while (linesAbove > 0);
1800: }
1801: if (newTopLine == null) {
1802: Line prev = begin.previousVisible();
1803: newTopLine = prev != null ? prev : begin;
1804: }
1805: if (topLine != newTopLine) {
1806: setTopLine(newTopLine);
1807: setUpdateFlag(REPAINT);
1808: }
1809: }
1810:
1811: private boolean isLineVisible(Line line) {
1812: return (line.lineNumber() >= getTopLineNumber() && line
1813: .lineNumber() < getTopLineNumber() + getRows());
1814: }
1815:
1816: private final int getMaxCols() {
1817: // We need some slack here (runs of italics tend to get compressed).
1818: // An extra 25% should be plenty.
1819: return (getWidth() / charWidth) * 5 / 4;
1820: }
1821:
1822: public final int getColumns() {
1823: return (getWidth() - getGutterWidth(editor.getBuffer()))
1824: / charWidth - 1;
1825: }
1826:
1827: public final int getRows() {
1828: return getHeight() / charHeight;
1829: }
1830:
1831: public void moveCaretToPoint(Point point) {
1832: final Position dot = editor.getDot();
1833: if (dot == null)
1834: return;
1835: final Line line = lineFromY(point.y);
1836: if (line == null)
1837: return;
1838: if (line != dot.getLine()) {
1839: editor.updateDotLine();
1840: dot.setLine(line);
1841: }
1842: caretCol = Math.max(getColumn(line, point.x), 0);
1843: editor.moveDotToCol(caretCol + shift);
1844: }
1845:
1846: public synchronized Position positionFromPoint(Point point,
1847: int shift) {
1848: int savedShift = this .shift;
1849: this .shift = shift;
1850: Position pos = positionFromPoint(point);
1851: this .shift = savedShift;
1852: return pos;
1853: }
1854:
1855: public Position positionFromPoint(Point point) {
1856: return positionFromPoint(point.x, point.y);
1857: }
1858:
1859: public Position positionFromPoint(int x, int y) {
1860: Line line = lineFromY(y);
1861: if (line == null)
1862: return null;
1863: Position pos = new Position(line, 0);
1864: int col = getColumn(line, x);
1865: pos.moveToCol(col + shift, editor.getBuffer().getTabWidth());
1866: return pos;
1867: }
1868:
1869: // y is offset from top of window.
1870: public Line lineFromY(int y) {
1871: if (topLine == null)
1872: return null;
1873: Line line = topLine;
1874: int total = -pixelsAboveTopLine;
1875: final int limit = getHeight();
1876: while (true) {
1877: total += line.getHeight();
1878: if (total > y)
1879: break;
1880: if (total > limit)
1881: break;
1882: Line next = line.nextVisible();
1883: if (next == null)
1884: break;
1885: line = next;
1886: }
1887: return line;
1888: }
1889:
1890: // y is absolute offset from start of buffer.
1891: private Line lineFromAbsoluteY(int y) {
1892: Line line = editor.getBuffer().getFirstLine();
1893: if (line != null) {
1894: int total = 0;
1895: while (true) {
1896: total += line.getHeight();
1897: if (total > y)
1898: break;
1899: Line next = line.nextVisible();
1900: if (next != null)
1901: line = line.nextVisible();
1902: else
1903: break;
1904: }
1905: }
1906: return line;
1907: }
1908:
1909: public synchronized int getColumn(Line line, int x) {
1910: if (line instanceof ImageLine)
1911: return 0;
1912: int maxCols = getMaxCols();
1913: formatLine(line, shift, maxCols);
1914: Graphics2D g2d = (Graphics2D) getGraphics();
1915: int begin = 0;
1916: int end = maxCols;
1917: while (end - begin > 4) {
1918: int pivot = (begin + end) / 2;
1919: int width = measureLine(g2d, textArray, pivot, formatArray);
1920: if (width + gutterWidth > x)
1921: end = pivot + 1;
1922: else
1923: begin = pivot - 1;
1924: }
1925: for (int i = begin; i < end; i++) {
1926: int width = measureLine(g2d, textArray, i, formatArray);
1927: if (width + gutterWidth > x)
1928: return i - 1;
1929: }
1930: return 0; // Shouldn't happen.
1931: }
1932:
1933: public boolean isOpaque() {
1934: return true;
1935: }
1936:
1937: public synchronized final void lineChanged(Line line) {
1938: // Avoid NPE in Hashtable.put().
1939: if (line == null) {
1940: Debug.bug("lineChanged line is null");
1941: return;
1942: }
1943: changedLines.put(line, line);
1944: }
1945:
1946: public static void resetDisplay() {
1947: if (plainFont == null)
1948: return; // Not initialized yet. Nothing to do.
1949: initializeStaticValues();
1950: for (EditorIterator it = new EditorIterator(); it.hasNext();) {
1951: Display display = it.nextEditor().getDisplay();
1952: display.initialize();
1953: display.repaint();
1954: }
1955: }
1956:
1957: public static void setRenderingHints(Graphics g) {
1958: if (antialias) {
1959: Graphics2D g2d = (Graphics2D) g;
1960: g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING,
1961: RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
1962: }
1963: }
1964:
1965: public String getToolTipText(MouseEvent e) {
1966: return editor.getMode().getToolTipText(editor, e);
1967: }
1968: }
|