tuned;
authorwenzelm
Wed, 05 Aug 2015 20:03:22 +0200
changeset 60847 239d7714392b
parent 60846 a7e3f11c19b7
child 60848 7ec20b1c8dc9
tuned;
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 {