Move ctrl-tab and ctrl-shift-tab handling into EditorHeader

Previously, EditorListener handled these keys, by registering a handler
in the text area. This meant that they would only work while the text
area was focused. By registering the keys as WHEN_IN_FOCUSED_WINDOW
bindings, they can always be handled, and EditorHeader seems like a more
appropriate place.

Note that this does not currently work (so this commit breaks these
keys), since these keys are also handled in a few different places as
well, preventing these newly added keybindings to take effect. This will
be fixed in the next commit.

One additional change is that previously, these keybindings did not work
when the text area was readonly. This was probably a remnant from when
EditorListener took care of a lot of other editing keybindings, but
this does not make much sense anymore now.

Finally, with the old bindings, ctrl-shift-tab did not (seem to) work.
What happened is that the binding for ctrl-tab did not check the shift
state, so both bindings would fire on ctrl-shift-tab, switching forward
and back again, making it seem the keys did not work. The Swing
keybinding mechanism that is now used for these bindings checks the
complete keystroke, including all modifier keys, so this problem is
fixed by this change.

References arduino#195

Author: matthijskooijman

app/src/processing/app/EditorHeader.java

@@ -110,6 +110,10 @@ public class Actions {
       Keys.bind(EditorHeader.this, newTab);
       Keys.bind(EditorHeader.this, prevTab);
       Keys.bind(EditorHeader.this, nextTab);
+
+      // Add alternative keybindings to switch tabs
+      Keys.bind(EditorHeader.this, prevTab, Keys.ctrlShift(KeyEvent.VK_TAB));
+      Keys.bind(EditorHeader.this, nextTab, Keys.ctrl(KeyEvent.VK_TAB));
     }
   }
   public Actions actions = new Actions();

app/src/processing/app/EditorListener.java

@@ -34,31 +34,6 @@ public void keyTyped(KeyEvent event) {
 
   @Override
   public void keyPressed(KeyEvent event) {
-
-    SketchTextArea textarea = editor.getTextArea();
-    
-    if (!textarea.isEditable()) return;
-    
-    Sketch sketch = editor.getSketch();
-
-    int code = event.getKeyCode();
-    
-    // Navigation..
-    if ((event.getModifiers() & CTRL) == CTRL && code == KeyEvent.VK_TAB) {
-      sketch.handleNextCode();
-    }
-
-    // Navigation..
-    // FIXME: not working on LINUX !!!
-    if ((event.getModifiers() & CTRL_SHIFT) == CTRL_SHIFT && code == KeyEvent.VK_TAB) {
-        sketch.handlePrevCode();
-    }
-    
-//    if (event.isAltDown() && code == KeyEvent.VK_T) {
-//      int line = textarea.getCaretLineNumber();
-//      textarea.setActiveLineRange(line, line + 3); 
-//    }
-    
   }
 
   @Override