From a2111fdcf666392d549916c3ff4b8d7607c66251 Mon Sep 17 00:00:00 2001 From: Cayci Date: Mon, 28 Oct 2013 21:01:35 -0400 Subject: [PATCH] add preference to enable/disable line numbers add preference to enable/disable line numbers and make font change work --- app/src/processing/app/Editor.java | 3 ++ app/src/processing/app/Preferences.java | 12 +++++ .../processing/app/syntax/JEditTextArea.java | 10 ++++- .../app/syntax/TextAreaLineNumbers.java | 44 ++++++++++++++----- build/shared/lib/preferences.txt | 3 ++ 5 files changed, 59 insertions(+), 13 deletions(-) diff --git a/app/src/processing/app/Editor.java b/app/src/processing/app/Editor.java index 774d20f74..1224cc760 100644 --- a/app/src/processing/app/Editor.java +++ b/app/src/processing/app/Editor.java @@ -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) { @@ -450,6 +452,7 @@ public class Editor extends JFrame implements RunnerListener { // apply changes to the font size for the editor //TextAreaPainter painter = textarea.getPainter(); painter.setFont(Preferences.getFont("editor.font")); + textarea.setLineNumbersFont(Preferences.getFont("editor.font")); //Font font = painter.getFont(); //textarea.getPainter().setFont(new Font("Courier", Font.PLAIN, 36)); diff --git a/app/src/processing/app/Preferences.java b/app/src/processing/app/Preferences.java index 00a5989ed..e084ddde6 100644 --- a/app/src/processing/app/Preferences.java +++ b/app/src/processing/app/Preferences.java @@ -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. diff --git a/app/src/processing/app/syntax/JEditTextArea.java b/app/src/processing/app/syntax/JEditTextArea.java index 1a8b5c204..36fd20c7b 100644 --- a/app/src/processing/app/syntax/JEditTextArea.java +++ b/app/src/processing/app/syntax/JEditTextArea.java @@ -87,7 +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()); + editorLineNumbers = new TextAreaLineNumbers(defaults, (int) painter.getPreferredSize().getHeight()); documentHandler = new DocumentHandler(); eventListenerList = new EventListenerList(); caretEvent = new MutableCaretEvent(); @@ -2427,4 +2427,12 @@ public class JEditTextArea extends JComponent caretTimer.setInitialDelay(500); caretTimer.start(); } + + public void setDisplayLineNumbers(boolean displayLineNumbers) { + editorLineNumbers.setDisplayLineNumbers(displayLineNumbers); + } + + public void setLineNumbersFont(Font font) { + editorLineNumbers.setTextFont(font); + } } diff --git a/app/src/processing/app/syntax/TextAreaLineNumbers.java b/app/src/processing/app/syntax/TextAreaLineNumbers.java index acc08d9dd..e374062dc 100644 --- a/app/src/processing/app/syntax/TextAreaLineNumbers.java +++ b/app/src/processing/app/syntax/TextAreaLineNumbers.java @@ -16,9 +16,12 @@ import java.awt.Rectangle; import javax.swing.JTextPane; import javax.swing.border.MatteBorder; +import javax.swing.text.AttributeSet; import javax.swing.text.SimpleAttributeSet; import javax.swing.text.StyleConstants; +import processing.app.Preferences; + public class TextAreaLineNumbers extends JTextPane { private final int LEFT_INDENT = 6; @@ -34,26 +37,30 @@ public class TextAreaLineNumbers extends JTextPane { 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); + public TextAreaLineNumbers(TextAreaDefaults defaults, int preferredHeight) { + setBackground(defaults.bgcolor); + setForeground(defaults.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); + setTextFont(Preferences.getFont("editor.font")); DIGIT_WIDTH = getFontMetrics(getFont()).stringWidth("0"); MIN_WIDTH = DIGIT_WIDTH * MIN_NUM_DIGITS + PADDING_WIDTH; 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) { if (currStartNum == startNum && currEndNum == endNum) { @@ -68,7 +75,7 @@ public class TextAreaLineNumbers extends JTextPane { } sb.append(endNum); setText(sb.toString()); - + invalidate(); } @@ -78,8 +85,21 @@ public class TextAreaLineNumbers extends JTextPane { } currNumDigits = numDigits; - setBounds(new Rectangle(Math.max(MIN_WIDTH, DIGIT_WIDTH * numDigits + PADDING_WIDTH), getHeight())); + updateBounds(); + 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())); + } } diff --git a/build/shared/lib/preferences.txt b/build/shared/lib/preferences.txt index 67246f860..f9bac321b 100755 --- a/build/shared/lib/preferences.txt +++ b/build/shared/lib/preferences.txt @@ -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