|
26 | 26 | import javax.swing.*;
|
27 | 27 | import javax.swing.text.*;
|
28 | 28 | import java.awt.*;
|
| 29 | +import java.awt.event.KeyAdapter; |
| 30 | +import java.awt.event.KeyEvent; |
| 31 | +import java.awt.event.MouseWheelEvent; |
29 | 32 | import java.io.PrintStream;
|
30 | 33 |
|
31 | 34 | import static processing.app.Theme.scale;
|
@@ -61,7 +64,7 @@ public static void setCurrentEditorConsole(EditorConsole console) {
|
61 | 64 | private SimpleAttributeSet stdOutStyle;
|
62 | 65 | private SimpleAttributeSet stdErrStyle;
|
63 | 66 |
|
64 |
| - public EditorConsole() { |
| 67 | + public EditorConsole(final Base base) { |
65 | 68 | document = new DefaultStyledDocument();
|
66 | 69 |
|
67 | 70 | consoleTextPane = new JTextPane(document);
|
@@ -110,6 +113,40 @@ public EditorConsole() {
|
110 | 113 | setMinimumSize(new Dimension(100, (height * lines)));
|
111 | 114 |
|
112 | 115 | EditorConsole.init(stdOutStyle, System.out, stdErrStyle, System.err);
|
| 116 | + |
| 117 | + // Add "CTRL scroll" hotkey for font size adjustment. |
| 118 | + consoleTextPane.addMouseWheelListener((MouseWheelEvent e) -> { |
| 119 | + if (e.isControlDown()) { |
| 120 | + if (e.getWheelRotation() < 0) { |
| 121 | + base.handleFontSizeChange(1); |
| 122 | + } else { |
| 123 | + base.handleFontSizeChange(-1); |
| 124 | + } |
| 125 | + } else { |
| 126 | + e.getComponent().getParent().dispatchEvent(e); |
| 127 | + } |
| 128 | + }); |
| 129 | + |
| 130 | + // Add "CTRL (SHIFT) =/+" and "CTRL -" hotkeys for font size adjustment. |
| 131 | + consoleTextPane.addKeyListener(new KeyAdapter() { |
| 132 | + @Override |
| 133 | + public void keyPressed(KeyEvent e) { |
| 134 | + if (e.getModifiersEx() == KeyEvent.CTRL_DOWN_MASK |
| 135 | + || e.getModifiersEx() == (KeyEvent.CTRL_DOWN_MASK | KeyEvent.SHIFT_DOWN_MASK)) { |
| 136 | + switch (e.getKeyCode()) { |
| 137 | + case KeyEvent.VK_PLUS: |
| 138 | + case KeyEvent.VK_EQUALS: |
| 139 | + base.handleFontSizeChange(1); |
| 140 | + break; |
| 141 | + case KeyEvent.VK_MINUS: |
| 142 | + if (!e.isShiftDown()) { |
| 143 | + base.handleFontSizeChange(-1); |
| 144 | + } |
| 145 | + break; |
| 146 | + } |
| 147 | + } |
| 148 | + } |
| 149 | + }); |
113 | 150 | }
|
114 | 151 |
|
115 | 152 | public void applyPreferences() {
|
|
0 commit comments