no keyboard control -- avoid confusion about meaning of selection;

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