From 87715edddd39484fe050b2d80f2aefa3b8f154a4 Mon Sep 17 00:00:00 2001 From: benfry Date: Wed, 26 Sep 2007 09:48:36 +0000 Subject: [PATCH] more space for prefs dialog on linux, also fix ctrl-, problem --- app/src/processing/app/EditorListener.java | 15 +++++++++++++-- app/src/processing/app/Preferences.java | 11 ++++++----- app/src/processing/app/syntax/JEditTextArea.java | 5 +++-- 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/app/src/processing/app/EditorListener.java b/app/src/processing/app/EditorListener.java index d6e8f33b4..677db87f4 100644 --- a/app/src/processing/app/EditorListener.java +++ b/app/src/processing/app/EditorListener.java @@ -93,6 +93,7 @@ public class EditorListener { * Called by JEditTextArea inside processKeyEvent(). Note that this * won't intercept actual characters, because those are fired on * keyTyped(). + * @return true if the event has been handled (to remove it from the queue) */ public boolean keyPressed(KeyEvent event) { // don't do things if the textarea isn't editable @@ -504,11 +505,20 @@ public class EditorListener { //static final int CTRL_ALT = ActionEvent.ALT_MASK | // Toolkit.getDefaultToolkit().getMenuShortcutKeyMask(); - /* public boolean keyTyped(KeyEvent event) { char c = event.getKeyChar(); int code = event.getKeyCode(); + if ((event.getModifiers() & KeyEvent.CTRL_MASK) != 0) { + // on linux, ctrl-comma (prefs) being passed through to the editor + if (c == KeyEvent.VK_COMMA) { + event.consume(); + return true; + } + } + return false; + + /* if ((event.getModifiers() & CMD_ALT) == CMD_ALT) { if (code == KeyEvent.VK_LEFT) { //if (c == '[') { @@ -521,8 +531,9 @@ public class EditorListener { } } return false; + */ } - */ + /** diff --git a/app/src/processing/app/Preferences.java b/app/src/processing/app/Preferences.java index 8493be20b..bb1074e60 100644 --- a/app/src/processing/app/Preferences.java +++ b/app/src/processing/app/Preferences.java @@ -223,7 +223,8 @@ public class Preferences { new JCheckBox("Use multiple .jar files when exporting applets"); pain.add(exportSeparateBox); d = exportSeparateBox.getPreferredSize(); - exportSeparateBox.setBounds(left, top, d.width, d.height); + // adding +10 because ubuntu + jre 1.5 truncating items + exportSeparateBox.setBounds(left, top, d.width + 10, d.height); right = Math.max(right, left + d.width); top += d.height + GUI_BETWEEN; @@ -234,7 +235,7 @@ public class Preferences { new JCheckBox("Prompt for name when opening or creating a sketch"); pain.add(sketchPromptBox); d = sketchPromptBox.getPreferredSize(); - sketchPromptBox.setBounds(left, top, d.width, d.height); + sketchPromptBox.setBounds(left, top, d.width + 10, d.height); right = Math.max(right, left + d.width); top += d.height + GUI_BETWEEN; @@ -244,7 +245,7 @@ public class Preferences { sketchCleanBox = new JCheckBox("Delete empty sketches on Quit"); pain.add(sketchCleanBox); d = sketchCleanBox.getPreferredSize(); - sketchCleanBox.setBounds(left, top, d.width, d.height); + sketchCleanBox.setBounds(left, top, d.width + 10, d.height); right = Math.max(right, left + d.width); top += d.height + GUI_BETWEEN; @@ -339,7 +340,7 @@ public class Preferences { externalEditorBox = new JCheckBox("Use external editor"); pain.add(externalEditorBox); d = externalEditorBox.getPreferredSize(); - externalEditorBox.setBounds(left, top, d.width, d.height); + externalEditorBox.setBounds(left, top, d.width + 10, d.height); right = Math.max(right, left + d.width); top += d.height + GUI_BETWEEN; @@ -349,7 +350,7 @@ public class Preferences { checkUpdatesBox = new JCheckBox("Check for updates on startup"); pain.add(checkUpdatesBox); d = checkUpdatesBox.getPreferredSize(); - checkUpdatesBox.setBounds(left, top, d.width, d.height); + checkUpdatesBox.setBounds(left, top, d.width + 10, d.height); right = Math.max(right, left + d.width); top += d.height + GUI_BETWEEN; diff --git a/app/src/processing/app/syntax/JEditTextArea.java b/app/src/processing/app/syntax/JEditTextArea.java index 96d8fe5f6..bbe6aabe3 100644 --- a/app/src/processing/app/syntax/JEditTextArea.java +++ b/app/src/processing/app/syntax/JEditTextArea.java @@ -1642,8 +1642,9 @@ public class JEditTextArea extends JComponent switch(evt.getID()) { case KeyEvent.KEY_TYPED: - //if ((editorListener != null) && !editorListener.keyTyped(evt)) { - inputHandler.keyTyped(evt); + if ((editorListener != null) && !editorListener.keyTyped(evt)) { + inputHandler.keyTyped(evt); + } break; case KeyEvent.KEY_PRESSED: if ((editorListener != null) && !editorListener.keyPressed(evt)) {