You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@groovy.apache.org by su...@apache.org on 2021/06/12 16:49:35 UTC
[groovy] branch master updated: Trivial tweak for setting preferred
size of numbers panel
This is an automated email from the ASF dual-hosted git repository.
sunlan pushed a commit to branch master
in repository https://gitbox.apache.org/repos/asf/groovy.git
The following commit(s) were added to refs/heads/master by this push:
new 134ed00 Trivial tweak for setting preferred size of numbers panel
134ed00 is described below
commit 134ed00cd26a8df6155cbea50cbc13f2172715de
Author: Daniel Sun <su...@apache.org>
AuthorDate: Sun Jun 13 00:48:42 2021 +0800
Trivial tweak for setting preferred size of numbers panel
---
.../src/main/groovy/groovy/console/ui/ConsoleTextEditor.java | 10 +++-------
1 file changed, 3 insertions(+), 7 deletions(-)
diff --git a/subprojects/groovy-console/src/main/groovy/groovy/console/ui/ConsoleTextEditor.java b/subprojects/groovy-console/src/main/groovy/groovy/console/ui/ConsoleTextEditor.java
index 8f9f2fa..7b15f77 100644
--- a/subprojects/groovy-console/src/main/groovy/groovy/console/ui/ConsoleTextEditor.java
+++ b/subprojects/groovy-console/src/main/groovy/groovy/console/ui/ConsoleTextEditor.java
@@ -159,6 +159,9 @@ public class ConsoleTextEditor extends JScrollPane {
fs = DEFAULT_FONT_SIZE;
}
fontSize = fs;
+
+ int width = 3 * fontSize;
+ numbersPanel.setPreferredSize(new Dimension(width, width));
}
});
textEditor.setFont(new Font(defaultFamily, Font.PLAIN, fontSize));
@@ -181,8 +184,6 @@ public class ConsoleTextEditor extends JScrollPane {
// add a document listener, to hint whether the line number gutter has to be repainted
// when the number of lines changes
doc.addDocumentListener(new DocumentListener() {
- private int width;
-
@Override
public void insertUpdate(DocumentEvent documentEvent) {
documentChangedSinceLastRepaint = true;
@@ -196,11 +197,6 @@ public class ConsoleTextEditor extends JScrollPane {
@Override
public void changedUpdate(DocumentEvent documentEvent) {
documentChangedSinceLastRepaint = true;
- int width = 3 * fontSize;
- if (width != this.width) {
- this.width = width;
- numbersPanel.setPreferredSize(new Dimension(width, width));
- }
}
});