# HG changeset patch
# User wenzelm
# Date 1438797802 -7200
# Node ID 239d7714392b9e321c8bdde0738f925dd47ca437
# Parent  a7e3f11c19b71aa44de76888a6e5c1bce15fc3e8
tuned;

diff -r a7e3f11c19b7 -r 239d7714392b src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Wed Aug 05 20:02:44 2015 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Wed Aug 05 20:03:22 2015 +0200
@@ -9,9 +9,9 @@
 
 import isabelle._
 
-import java.awt.{Dimension, GridLayout}
+import java.awt.Dimension
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
-import javax.swing.{JTree, JScrollPane, JComponent}
+import javax.swing.{JTree, JScrollPane}
 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
 
@@ -47,11 +47,10 @@
 
   private val tree = new JTree(root)
   tree.setRowHeight(0)
+  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
 
   override def focusOnDefaultComponent { tree.requestFocusInWindow }
 
-  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
-
   private def action(node: DefaultMutableTreeNode)
   {
     node.getUserObject match {