# HG changeset patch
# User wenzelm
# Date 1398519193 -7200
# Node ID 72b4205f4de9dda734b4fdd3348ce734a59d62c4
# Parent  2080e752ed4029d5c40ccd83753fa8655a0b0601
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;

diff -r 2080e752ed40 -r 72b4205f4de9 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sat Apr 26 15:01:42 2014 +0200
+++ b/src/Pure/GUI/gui.scala	Sat Apr 26 15:33:13 2014 +0200
@@ -9,10 +9,10 @@
 
 
 import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
-import java.awt.{Image, Component, Container, Toolkit, Window, Font}
+import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
 import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JButton}
 
 import scala.collection.convert.WrapAsJava
 import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -39,6 +39,18 @@
     UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
 
 
+  /* plain focus traversal, notably for text fields */
+
+  def plain_focus_traversal(component: Component)
+  {
+    val dummy_button = new JButton
+    def apply(id: Int): Unit =
+      component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
+    apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
+    apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
+  }
+
+
   /* X11 window manager */
 
   def window_manager(): Option[String] =
diff -r 2080e752ed40 -r 72b4205f4de9 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Apr 26 15:01:42 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Apr 26 15:33:13 2014 +0200
@@ -93,6 +93,7 @@
               case _ => true
             }
           })
+        GUI.plain_focus_traversal(text_area.peer)
         text_area
       }
     component.load()