mirror of
https://github.com/arduino/Arduino.git
synced 2025-01-30 19:52:13 +01:00
Merge branch 'cayci-master'
This commit is contained in:
commit
89d6841ac0
@ -430,6 +430,8 @@ public class Editor extends JFrame implements RunnerListener {
|
||||
textarea.setEditable(!external);
|
||||
saveMenuItem.setEnabled(!external);
|
||||
saveAsMenuItem.setEnabled(!external);
|
||||
|
||||
textarea.setDisplayLineNumbers(Preferences.getBoolean("editor.linenumbers"));
|
||||
|
||||
TextAreaPainter painter = textarea.getPainter();
|
||||
if (external) {
|
||||
|
@ -177,6 +177,7 @@ public class Preferences {
|
||||
JCheckBox exportSeparateBox;
|
||||
JCheckBox verboseCompilationBox;
|
||||
JCheckBox verboseUploadBox;
|
||||
JCheckBox displayLineNumbersBox;
|
||||
JCheckBox verifyUploadBox;
|
||||
JCheckBox externalEditorBox;
|
||||
JCheckBox memoryOverrideBox;
|
||||
@ -382,6 +383,15 @@ public class Preferences {
|
||||
box.setBounds(left, top, d.width, d.height);
|
||||
top += d.height + GUI_BETWEEN;
|
||||
|
||||
// [ ] Display line numbers
|
||||
|
||||
displayLineNumbersBox = new JCheckBox(_("Display line numbers"));
|
||||
pain.add(displayLineNumbersBox);
|
||||
d = displayLineNumbersBox.getPreferredSize();
|
||||
displayLineNumbersBox.setBounds(left, top, d.width + 10, d.height);
|
||||
right = Math.max(right, left + d.width);
|
||||
top += d.height + GUI_BETWEEN;
|
||||
|
||||
// [ ] Verify code after upload
|
||||
|
||||
verifyUploadBox = new JCheckBox(_("Verify code after upload"));
|
||||
@ -571,6 +581,7 @@ public class Preferences {
|
||||
// put each of the settings into the table
|
||||
setBoolean("build.verbose", verboseCompilationBox.isSelected());
|
||||
setBoolean("upload.verbose", verboseUploadBox.isSelected());
|
||||
setBoolean("editor.linenumbers", displayLineNumbersBox.isSelected());
|
||||
setBoolean("upload.verify", verifyUploadBox.isSelected());
|
||||
|
||||
// setBoolean("sketchbook.closing_last_window_quits",
|
||||
@ -634,6 +645,7 @@ public class Preferences {
|
||||
// set all settings entry boxes to their actual status
|
||||
verboseCompilationBox.setSelected(getBoolean("build.verbose"));
|
||||
verboseUploadBox.setSelected(getBoolean("upload.verbose"));
|
||||
displayLineNumbersBox.setSelected(getBoolean("editor.linenumbers"));
|
||||
verifyUploadBox.setSelected(getBoolean("upload.verify"));
|
||||
|
||||
//closingLastQuitsBox.
|
||||
|
@ -87,6 +87,7 @@ public class JEditTextArea extends JComponent
|
||||
|
||||
// Initialize some misc. stuff
|
||||
painter = new TextAreaPainter(this,defaults);
|
||||
editorLineNumbers = new TextAreaLineNumbers(this,defaults);
|
||||
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,14 @@ public class JEditTextArea extends JComponent
|
||||
horizontal.setUnitIncrement(charWidth);
|
||||
horizontal.setBlockIncrement(width / 2);
|
||||
}
|
||||
updateLineNumbers();
|
||||
}
|
||||
|
||||
private void updateLineNumbers() {
|
||||
if (editorLineNumbers != null) {
|
||||
editorLineNumbers.updateLineNumbers(getFirstLine() + 1, Math.min(getFirstLine() + getVisibleLines() + 1, getLineCount()));
|
||||
editorLineNumbers.updateWidthForNumDigits(String.valueOf(getLineCount()).length());
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
@ -335,7 +345,7 @@ public class JEditTextArea extends JComponent
|
||||
if (firstLine != vertical.getValue()) {
|
||||
updateScrollBars();
|
||||
}
|
||||
painter.repaint();
|
||||
repaintEditor();
|
||||
}
|
||||
|
||||
/**
|
||||
@ -377,7 +387,7 @@ public class JEditTextArea extends JComponent
|
||||
this.horizontalOffset = horizontalOffset;
|
||||
if(horizontalOffset != horizontal.getValue())
|
||||
updateScrollBars();
|
||||
painter.repaint();
|
||||
repaintEditor();
|
||||
}
|
||||
|
||||
/**
|
||||
@ -407,12 +417,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 +747,7 @@ public class JEditTextArea extends JComponent
|
||||
|
||||
select(0, 0);
|
||||
updateScrollBars();
|
||||
painter.repaint();
|
||||
repaintEditor();
|
||||
}
|
||||
|
||||
|
||||
@ -753,7 +768,7 @@ public class JEditTextArea extends JComponent
|
||||
select(start, stop);
|
||||
updateScrollBars();
|
||||
setScrollPosition(scroll);
|
||||
painter.repaint();
|
||||
repaintEditor();
|
||||
}
|
||||
|
||||
|
||||
@ -790,7 +805,11 @@ public class JEditTextArea extends JComponent
|
||||
*/
|
||||
public final int getLineCount()
|
||||
{
|
||||
return document.getDefaultRootElement().getElementCount();
|
||||
if (document != null) {
|
||||
return document.getDefaultRootElement().getElementCount();
|
||||
} else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
@ -1747,6 +1766,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 +1775,7 @@ public class JEditTextArea extends JComponent
|
||||
protected static Timer caretTimer;
|
||||
|
||||
protected TextAreaPainter painter;
|
||||
protected TextAreaLineNumbers editorLineNumbers;
|
||||
|
||||
//protected EditPopupMenu popup;
|
||||
protected JPopupMenu popup;
|
||||
@ -1881,7 +1902,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 +1916,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 +1938,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 +1958,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 +1979,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 +2021,7 @@ public class JEditTextArea extends JComponent
|
||||
}
|
||||
|
||||
// private members
|
||||
private Component left;
|
||||
private Component center;
|
||||
private Component right;
|
||||
private Component bottom;
|
||||
@ -2395,4 +2433,8 @@ public class JEditTextArea extends JComponent
|
||||
caretTimer.setInitialDelay(500);
|
||||
caretTimer.start();
|
||||
}
|
||||
|
||||
public void setDisplayLineNumbers(boolean displayLineNumbers) {
|
||||
editorLineNumbers.setDisplayLineNumbers(displayLineNumbers);
|
||||
}
|
||||
}
|
||||
|
106
app/src/processing/app/syntax/TextAreaLineNumbers.java
Normal file
106
app/src/processing/app/syntax/TextAreaLineNumbers.java
Normal file
@ -0,0 +1,106 @@
|
||||
/*
|
||||
* 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.Graphics;
|
||||
import java.awt.Rectangle;
|
||||
|
||||
import javax.swing.border.MatteBorder;
|
||||
|
||||
public class TextAreaLineNumbers extends TextAreaPainter {
|
||||
|
||||
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(JEditTextArea textArea, TextAreaDefaults defaults) {
|
||||
super(textArea, defaults);
|
||||
DIGIT_WIDTH = getFontMetrics(getFont()).stringWidth("0");
|
||||
MIN_WIDTH = DIGIT_WIDTH * MIN_NUM_DIGITS + PADDING_WIDTH;
|
||||
setEnabled(false);
|
||||
setBorder(new MatteBorder(0, 0, 0, RIGHT_BORDER_WIDTH, new Color(240, 240, 240)));
|
||||
}
|
||||
|
||||
public void updateLineNumbers(int startNum, int endNum) {
|
||||
if (currStartNum == startNum && currEndNum == endNum) {
|
||||
return;
|
||||
}
|
||||
currStartNum = startNum;
|
||||
currEndNum = endNum;
|
||||
|
||||
invalidate();
|
||||
repaint();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void paint(Graphics gfx) {
|
||||
super.paint(gfx);
|
||||
getBorder().paintBorder(this, gfx, 0, 0, getSize().width, getSize().height);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void paintLine(Graphics gfx, TokenMarker tokenMarker,
|
||||
int line, int x)
|
||||
{
|
||||
currentLineIndex = line;
|
||||
gfx.setFont(getFont());
|
||||
gfx.setColor(Color.GRAY);
|
||||
int y = textArea.lineToY(line);
|
||||
int startX = getBounds().x + getBounds().width;
|
||||
if (line >= 0 && line < textArea.getLineCount()) {
|
||||
String lineNumberString = String.valueOf(line+1);
|
||||
int lineStartX = startX - RIGHT_BORDER_WIDTH - RIGHT_INDENT - fm.stringWidth(lineNumberString);
|
||||
gfx.drawString(lineNumberString,lineStartX,y + fm.getHeight());
|
||||
}
|
||||
}
|
||||
|
||||
public void updateWidthForNumDigits(int numDigits) {
|
||||
if (currNumDigits == numDigits) {
|
||||
return;
|
||||
}
|
||||
currNumDigits = numDigits;
|
||||
|
||||
if (isVisible()) {
|
||||
updateBounds();
|
||||
invalidate();
|
||||
repaint();
|
||||
}
|
||||
}
|
||||
|
||||
public void setDisplayLineNumbers(boolean displayLineNumbers) {
|
||||
setVisible(displayLineNumbers);
|
||||
if (displayLineNumbers) {
|
||||
updateBounds();
|
||||
} else {
|
||||
setBounds(new Rectangle(0, getHeight()));
|
||||
}
|
||||
invalidate();
|
||||
repaint();
|
||||
}
|
||||
|
||||
private void updateBounds() {
|
||||
if (isVisible()) {
|
||||
setBounds(new Rectangle(Math.max(MIN_WIDTH, DIGIT_WIDTH * currNumDigits + PADDING_WIDTH), getHeight()));
|
||||
textArea.validate();
|
||||
}
|
||||
}
|
||||
}
|
@ -104,6 +104,9 @@ editor.caret.blink=true
|
||||
# area that's not in use by the text (replaced with tildes)
|
||||
editor.invalid=false
|
||||
|
||||
# show line numbers in editor
|
||||
editor.linenumbers = false
|
||||
|
||||
# enable ctrl-ins, shift-ins, shift-delete for cut/copy/paste
|
||||
# on windows and linux, but disable on the mac
|
||||
editor.keys.alternative_cut_copy_paste = true
|
||||
|
Loading…
x
Reference in New Issue
Block a user