rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2024-12-01 12:24:14 +01:00
Code Issues Releases Activity

Display line numbers for the file being edited

Browse Source
This commit is contained in:
Cayci 2013-10-28 00:19:30 -04:00
parent 128678c559
commit 787f73dade
2 changed files with 124 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
app/src/processing/app/syntax/JEditTextArea.java
View File

@ -87,6 +87,7 @@ public class JEditTextArea extends JComponent
// Initialize some misc. stuff
painter = new TextAreaPainter(this,defaults);
editorLineNumbers = new TextAreaLineNumbers(defaults.font, defaults.bgcolor, defaults.fgcolor, (int) painter.getPreferredSize().getHeight());
documentHandler = new DocumentHandler();
eventListenerList = new EventListenerList();
caretEvent = new MutableCaretEvent();
@ -96,6 +97,7 @@ public class JEditTextArea extends JComponent
// Initialize the GUI
setLayout(new ScrollLayout());
add(LEFT, editorLineNumbers);
add(CENTER, painter);
add(RIGHT, vertical = new JScrollBar(JScrollBar.VERTICAL));
add(BOTTOM, horizontal = new JScrollBar(JScrollBar.HORIZONTAL));
@ -315,6 +317,12 @@ public class JEditTextArea extends JComponent
horizontal.setUnitIncrement(charWidth);
horizontal.setBlockIncrement(width / 2);
}
updateLineNumbers();
}
private void updateLineNumbers() {
editorLineNumbers.updateLineNumbers(getFirstLine() + 1, Math.min(getFirstLine() + getVisibleLines() + 1, getLineCount()));
editorLineNumbers.updateWidthForNumDigits(String.valueOf(getLineCount()).length());
}
/**
@ -335,7 +343,7 @@ public class JEditTextArea extends JComponent
if (firstLine != vertical.getValue()) {
updateScrollBars();
}
painter.repaint();
repaintEditor();
}
/**
@ -377,7 +385,7 @@ public class JEditTextArea extends JComponent
this.horizontalOffset = horizontalOffset;
if(horizontalOffset != horizontal.getValue())
updateScrollBars();
painter.repaint();
repaintEditor();
}
/**
@ -407,12 +415,17 @@ public class JEditTextArea extends JComponent
if(changed)
{
updateScrollBars();
painter.repaint();
repaintEditor();
}
return changed;
}
private void repaintEditor() {
painter.repaint();
updateLineNumbers();
}
/**
* Ensures that the caret is visible by scrolling the text area if
* necessary.
@ -732,7 +745,7 @@ public class JEditTextArea extends JComponent
select(0, 0);
updateScrollBars();
painter.repaint();
repaintEditor();
}
@ -753,7 +766,7 @@ public class JEditTextArea extends JComponent
select(start, stop);
updateScrollBars();
setScrollPosition(scroll);
painter.repaint();
repaintEditor();
}
@ -1747,6 +1760,7 @@ public class JEditTextArea extends JComponent
}
// protected members
protected static String LEFT = "left";
protected static String CENTER = "center";
protected static String RIGHT = "right";
protected static String BOTTOM = "bottom";
@ -1755,6 +1769,7 @@ public class JEditTextArea extends JComponent
protected static Timer caretTimer;
protected TextAreaPainter painter;
protected TextAreaLineNumbers editorLineNumbers;
//protected EditPopupMenu popup;
protected JPopupMenu popup;
@ -1881,7 +1896,9 @@ public class JEditTextArea extends JComponent
public void addLayoutComponent(String name, Component comp)
{
if(name.equals(CENTER))
if(name.equals(LEFT))
left = comp;
else if(name.equals(CENTER))
center = comp;
else if(name.equals(RIGHT))
right = comp;
@ -1893,6 +1910,8 @@ public class JEditTextArea extends JComponent
public void removeLayoutComponent(Component comp)
{
if(left == comp)
left = null;
if(center == comp)
center = null;
if(right == comp)
@ -1913,6 +1932,8 @@ public class JEditTextArea extends JComponent
Dimension centerPref = center.getPreferredSize();
dim.width += centerPref.width;
dim.height += centerPref.height;
Dimension leftPref = left.getPreferredSize();
dim.width += leftPref.width;
Dimension rightPref = right.getPreferredSize();
dim.width += rightPref.width;
Dimension bottomPref = bottom.getPreferredSize();
@ -1931,6 +1952,8 @@ public class JEditTextArea extends JComponent
Dimension centerPref = center.getMinimumSize();
dim.width += centerPref.width;
dim.height += centerPref.height;
Dimension leftPref = left.getMinimumSize();
dim.width += leftPref.width;
Dimension rightPref = right.getMinimumSize();
dim.width += rightPref.width;
Dimension bottomPref = bottom.getMinimumSize();
@ -1950,11 +1973,19 @@ public class JEditTextArea extends JComponent
int ibottom = insets.bottom;
int iright = insets.right;
int leftWidth = left.getSize().width;
int rightWidth = right.getPreferredSize().width;
int bottomHeight = bottom.getPreferredSize().height;
int centerWidth = size.width - rightWidth - ileft - iright;
int centerWidth = size.width - leftWidth - rightWidth - ileft - iright;
int centerHeight = size.height - bottomHeight - itop - ibottom;
left.setBounds(ileft,
itop,
leftWidth,
centerHeight);
ileft += leftWidth;
center.setBounds(ileft, // + LEFT_EXTRA,
itop,
centerWidth, // - LEFT_EXTRA,
@ -1984,6 +2015,7 @@ public class JEditTextArea extends JComponent
}
// private members
private Component left;
private Component center;
private Component right;
private Component bottom;

85
app/src/processing/app/syntax/TextAreaLineNumbers.java Normal file
View File

@ -0,0 +1,85 @@
/*
* TextAreaLineNumbers.java - Show line numbers for the open file in the editor
* Copyright (C) 2013 Cayci Gorlitsky
*
* You may use and modify this package for any purpose. Redistribution is
* permitted, in both source and binary form, provided that this notice
* remains intact in all source distributions of this package.
*/
package processing.app.syntax;
import java.awt.Color;
import java.awt.Dimension;
import java.awt.Font;
import java.awt.Rectangle;
import javax.swing.JTextPane;
import javax.swing.border.MatteBorder;
import javax.swing.text.SimpleAttributeSet;
import javax.swing.text.StyleConstants;
public class TextAreaLineNumbers extends JTextPane {
private final int LEFT_INDENT = 6;
private final int RIGHT_INDENT = 6;
private final int RIGHT_BORDER_WIDTH = 1;
private final int PADDING_WIDTH = LEFT_INDENT + RIGHT_INDENT + RIGHT_BORDER_WIDTH;
private final int MIN_WIDTH;
private final int DIGIT_WIDTH;
private final int MIN_NUM_DIGITS = 2;
private int currStartNum = 0;
private int currEndNum = 0;
private int currNumDigits = MIN_NUM_DIGITS;
public TextAreaLineNumbers(Font font, Color bgcolor, Color fgcolor, int preferredHeight) {
setFont(font);
setBackground(bgcolor);
setForeground(fgcolor);
setOpaque(true);
setEditable(false);
setEnabled(false);
setBorder(new MatteBorder(0, 0, 0, 1, new Color(240, 240, 240)));
SimpleAttributeSet attribs = new SimpleAttributeSet();
StyleConstants.setAlignment(attribs , StyleConstants.ALIGN_RIGHT);
StyleConstants.setLeftIndent(attribs , 6);
StyleConstants.setRightIndent(attribs , 6);
setParagraphAttributes(attribs,true);
DIGIT_WIDTH = getFontMetrics(getFont()).stringWidth("0");
MIN_WIDTH = DIGIT_WIDTH * MIN_NUM_DIGITS + PADDING_WIDTH;
setPreferredSize(new Dimension(MIN_WIDTH, preferredHeight));
}
public void updateLineNumbers(int startNum, int endNum) {
if (currStartNum == startNum && currEndNum == endNum) {
return;
}
currStartNum = startNum;
currEndNum = endNum;
StringBuilder sb = new StringBuilder();
for (int i = startNum; i < endNum; i++) {
sb.append(i).append("\n");
}
sb.append(endNum);
setText(sb.toString());
invalidate();
}
public void updateWidthForNumDigits(int numDigits) {
if (currNumDigits == numDigits) {
return;
}
currNumDigits = numDigits;
setBounds(new Rectangle(Math.max(MIN_WIDTH, DIGIT_WIDTH * numDigits + PADDING_WIDTH), getHeight()));
invalidate();
}
}