# 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()