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