# HG changeset patch # User wenzelm # Date 1386369254 -3600 # Node ID 795f8d3e06c98ef38896b7d2d9ea38172825715c # Parent 070d5e8567983af1a75c2d7a0c97f5105b6f43a7 no keyboard control -- avoid confusion about meaning of selection; diff -r 070d5e856798 -r 795f8d3e06c9 src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Dec 06 23:25:38 2013 +0100 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Dec 06 23:34:14 2013 +0100 @@ -11,7 +11,7 @@ import java.awt.{Dimension, GridLayout} import java.awt.event.{MouseEvent, MouseAdapter} -import javax.swing.{JTree, JScrollPane} +import javax.swing.{JTree, JScrollPane, JComponent} import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel} import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} @@ -46,6 +46,12 @@ } private val tree = new JTree(root) + + for (cond <- + List(JComponent.WHEN_FOCUSED, + JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, + JComponent.WHEN_IN_FOCUSED_WINDOW)) tree.setInputMap(cond, null) + if (!OperatingSystem.isMacOSLF) tree.putClientProperty("JTree.lineStyle", "Angled") tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)