mirror of
https://github.com/arduino/Arduino.git
synced 2025-01-30 19:52:13 +01:00
add preference to enable/disable line numbers
add preference to enable/disable line numbers and make font change work
This commit is contained in:
parent
787f73dade
commit
a2111fdcf6
@ -431,6 +431,8 @@ public class Editor extends JFrame implements RunnerListener {
|
|||||||
saveMenuItem.setEnabled(!external);
|
saveMenuItem.setEnabled(!external);
|
||||||
saveAsMenuItem.setEnabled(!external);
|
saveAsMenuItem.setEnabled(!external);
|
||||||
|
|
||||||
|
textarea.setDisplayLineNumbers(Preferences.getBoolean("editor.linenumbers"));
|
||||||
|
|
||||||
TextAreaPainter painter = textarea.getPainter();
|
TextAreaPainter painter = textarea.getPainter();
|
||||||
if (external) {
|
if (external) {
|
||||||
// disable line highlight and turn off the caret when disabling
|
// disable line highlight and turn off the caret when disabling
|
||||||
@ -450,6 +452,7 @@ public class Editor extends JFrame implements RunnerListener {
|
|||||||
// apply changes to the font size for the editor
|
// apply changes to the font size for the editor
|
||||||
//TextAreaPainter painter = textarea.getPainter();
|
//TextAreaPainter painter = textarea.getPainter();
|
||||||
painter.setFont(Preferences.getFont("editor.font"));
|
painter.setFont(Preferences.getFont("editor.font"));
|
||||||
|
textarea.setLineNumbersFont(Preferences.getFont("editor.font"));
|
||||||
//Font font = painter.getFont();
|
//Font font = painter.getFont();
|
||||||
//textarea.getPainter().setFont(new Font("Courier", Font.PLAIN, 36));
|
//textarea.getPainter().setFont(new Font("Courier", Font.PLAIN, 36));
|
||||||
|
|
||||||
|
@ -177,6 +177,7 @@ public class Preferences {
|
|||||||
JCheckBox exportSeparateBox;
|
JCheckBox exportSeparateBox;
|
||||||
JCheckBox verboseCompilationBox;
|
JCheckBox verboseCompilationBox;
|
||||||
JCheckBox verboseUploadBox;
|
JCheckBox verboseUploadBox;
|
||||||
|
JCheckBox displayLineNumbersBox;
|
||||||
JCheckBox verifyUploadBox;
|
JCheckBox verifyUploadBox;
|
||||||
JCheckBox externalEditorBox;
|
JCheckBox externalEditorBox;
|
||||||
JCheckBox memoryOverrideBox;
|
JCheckBox memoryOverrideBox;
|
||||||
@ -380,6 +381,15 @@ public class Preferences {
|
|||||||
pain.add(box);
|
pain.add(box);
|
||||||
d = box.getPreferredSize();
|
d = box.getPreferredSize();
|
||||||
box.setBounds(left, top, d.width, d.height);
|
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;
|
top += d.height + GUI_BETWEEN;
|
||||||
|
|
||||||
// [ ] Verify code after upload
|
// [ ] Verify code after upload
|
||||||
@ -571,6 +581,7 @@ public class Preferences {
|
|||||||
// put each of the settings into the table
|
// put each of the settings into the table
|
||||||
setBoolean("build.verbose", verboseCompilationBox.isSelected());
|
setBoolean("build.verbose", verboseCompilationBox.isSelected());
|
||||||
setBoolean("upload.verbose", verboseUploadBox.isSelected());
|
setBoolean("upload.verbose", verboseUploadBox.isSelected());
|
||||||
|
setBoolean("editor.linenumbers", displayLineNumbersBox.isSelected());
|
||||||
setBoolean("upload.verify", verifyUploadBox.isSelected());
|
setBoolean("upload.verify", verifyUploadBox.isSelected());
|
||||||
|
|
||||||
// setBoolean("sketchbook.closing_last_window_quits",
|
// setBoolean("sketchbook.closing_last_window_quits",
|
||||||
@ -634,6 +645,7 @@ public class Preferences {
|
|||||||
// set all settings entry boxes to their actual status
|
// set all settings entry boxes to their actual status
|
||||||
verboseCompilationBox.setSelected(getBoolean("build.verbose"));
|
verboseCompilationBox.setSelected(getBoolean("build.verbose"));
|
||||||
verboseUploadBox.setSelected(getBoolean("upload.verbose"));
|
verboseUploadBox.setSelected(getBoolean("upload.verbose"));
|
||||||
|
displayLineNumbersBox.setSelected(getBoolean("editor.linenumbers"));
|
||||||
verifyUploadBox.setSelected(getBoolean("upload.verify"));
|
verifyUploadBox.setSelected(getBoolean("upload.verify"));
|
||||||
|
|
||||||
//closingLastQuitsBox.
|
//closingLastQuitsBox.
|
||||||
|
@ -87,7 +87,7 @@ public class JEditTextArea extends JComponent
|
|||||||
|
|
||||||
// Initialize some misc. stuff
|
// Initialize some misc. stuff
|
||||||
painter = new TextAreaPainter(this,defaults);
|
painter = new TextAreaPainter(this,defaults);
|
||||||
editorLineNumbers = new TextAreaLineNumbers(defaults.font, defaults.bgcolor, defaults.fgcolor, (int) painter.getPreferredSize().getHeight());
|
editorLineNumbers = new TextAreaLineNumbers(defaults, (int) painter.getPreferredSize().getHeight());
|
||||||
documentHandler = new DocumentHandler();
|
documentHandler = new DocumentHandler();
|
||||||
eventListenerList = new EventListenerList();
|
eventListenerList = new EventListenerList();
|
||||||
caretEvent = new MutableCaretEvent();
|
caretEvent = new MutableCaretEvent();
|
||||||
@ -2427,4 +2427,12 @@ public class JEditTextArea extends JComponent
|
|||||||
caretTimer.setInitialDelay(500);
|
caretTimer.setInitialDelay(500);
|
||||||
caretTimer.start();
|
caretTimer.start();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public void setDisplayLineNumbers(boolean displayLineNumbers) {
|
||||||
|
editorLineNumbers.setDisplayLineNumbers(displayLineNumbers);
|
||||||
|
}
|
||||||
|
|
||||||
|
public void setLineNumbersFont(Font font) {
|
||||||
|
editorLineNumbers.setTextFont(font);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -16,9 +16,12 @@ import java.awt.Rectangle;
|
|||||||
|
|
||||||
import javax.swing.JTextPane;
|
import javax.swing.JTextPane;
|
||||||
import javax.swing.border.MatteBorder;
|
import javax.swing.border.MatteBorder;
|
||||||
|
import javax.swing.text.AttributeSet;
|
||||||
import javax.swing.text.SimpleAttributeSet;
|
import javax.swing.text.SimpleAttributeSet;
|
||||||
import javax.swing.text.StyleConstants;
|
import javax.swing.text.StyleConstants;
|
||||||
|
|
||||||
|
import processing.app.Preferences;
|
||||||
|
|
||||||
public class TextAreaLineNumbers extends JTextPane {
|
public class TextAreaLineNumbers extends JTextPane {
|
||||||
|
|
||||||
private final int LEFT_INDENT = 6;
|
private final int LEFT_INDENT = 6;
|
||||||
@ -34,20 +37,14 @@ public class TextAreaLineNumbers extends JTextPane {
|
|||||||
private int currEndNum = 0;
|
private int currEndNum = 0;
|
||||||
private int currNumDigits = MIN_NUM_DIGITS;
|
private int currNumDigits = MIN_NUM_DIGITS;
|
||||||
|
|
||||||
public TextAreaLineNumbers(Font font, Color bgcolor, Color fgcolor, int preferredHeight) {
|
public TextAreaLineNumbers(TextAreaDefaults defaults, int preferredHeight) {
|
||||||
setFont(font);
|
setBackground(defaults.bgcolor);
|
||||||
setBackground(bgcolor);
|
setForeground(defaults.fgcolor);
|
||||||
setForeground(fgcolor);
|
|
||||||
setOpaque(true);
|
setOpaque(true);
|
||||||
setEditable(false);
|
setEditable(false);
|
||||||
setEnabled(false);
|
setEnabled(false);
|
||||||
setBorder(new MatteBorder(0, 0, 0, 1, new Color(240, 240, 240)));
|
setBorder(new MatteBorder(0, 0, 0, 1, new Color(240, 240, 240)));
|
||||||
|
setTextFont(Preferences.getFont("editor.font"));
|
||||||
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");
|
DIGIT_WIDTH = getFontMetrics(getFont()).stringWidth("0");
|
||||||
MIN_WIDTH = DIGIT_WIDTH * MIN_NUM_DIGITS + PADDING_WIDTH;
|
MIN_WIDTH = DIGIT_WIDTH * MIN_NUM_DIGITS + PADDING_WIDTH;
|
||||||
@ -55,6 +52,16 @@ public class TextAreaLineNumbers extends JTextPane {
|
|||||||
setPreferredSize(new Dimension(MIN_WIDTH, preferredHeight));
|
setPreferredSize(new Dimension(MIN_WIDTH, preferredHeight));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public void setTextFont(Font font) {
|
||||||
|
setFont(font);
|
||||||
|
SimpleAttributeSet attribs = new SimpleAttributeSet();
|
||||||
|
StyleConstants.setAlignment(attribs , StyleConstants.ALIGN_RIGHT);
|
||||||
|
StyleConstants.setLeftIndent(attribs , 6);
|
||||||
|
StyleConstants.setRightIndent(attribs , 6);
|
||||||
|
StyleConstants.setFontSize(attribs, getFont().getSize());
|
||||||
|
setParagraphAttributes(attribs,true);
|
||||||
|
}
|
||||||
|
|
||||||
public void updateLineNumbers(int startNum, int endNum) {
|
public void updateLineNumbers(int startNum, int endNum) {
|
||||||
if (currStartNum == startNum && currEndNum == endNum) {
|
if (currStartNum == startNum && currEndNum == endNum) {
|
||||||
return;
|
return;
|
||||||
@ -78,8 +85,21 @@ public class TextAreaLineNumbers extends JTextPane {
|
|||||||
}
|
}
|
||||||
currNumDigits = numDigits;
|
currNumDigits = numDigits;
|
||||||
|
|
||||||
setBounds(new Rectangle(Math.max(MIN_WIDTH, DIGIT_WIDTH * numDigits + PADDING_WIDTH), getHeight()));
|
updateBounds();
|
||||||
invalidate();
|
invalidate();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public void setDisplayLineNumbers(boolean displayLineNumbers) {
|
||||||
|
setVisible(displayLineNumbers);
|
||||||
|
if (displayLineNumbers) {
|
||||||
|
updateBounds();
|
||||||
|
} else {
|
||||||
|
setBounds(new Rectangle(0, getHeight()));
|
||||||
|
}
|
||||||
|
invalidate();
|
||||||
|
}
|
||||||
|
|
||||||
|
private void updateBounds() {
|
||||||
|
setBounds(new Rectangle(Math.max(MIN_WIDTH, DIGIT_WIDTH * currNumDigits + PADDING_WIDTH), getHeight()));
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -104,6 +104,9 @@ editor.caret.blink=true
|
|||||||
# area that's not in use by the text (replaced with tildes)
|
# area that's not in use by the text (replaced with tildes)
|
||||||
editor.invalid=false
|
editor.invalid=false
|
||||||
|
|
||||||
|
# show line numbers in editor
|
||||||
|
editor.linenumbers = false
|
||||||
|
|
||||||
# enable ctrl-ins, shift-ins, shift-delete for cut/copy/paste
|
# enable ctrl-ins, shift-ins, shift-delete for cut/copy/paste
|
||||||
# on windows and linux, but disable on the mac
|
# on windows and linux, but disable on the mac
|
||||||
editor.keys.alternative_cut_copy_paste = true
|
editor.keys.alternative_cut_copy_paste = true
|
||||||
|
Loading…
x
Reference in New Issue
Block a user