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