# HG changeset patch
# User wenzelm
# Date 1730664770 -3600
# Node ID 405f7fd15f4e771edb799e25fc094cd43c5edc24
# Parent  2239495a64f6252ba3bd40a596ac40cdc2816e94
tuned;

diff -r 2239495a64f6 -r 405f7fd15f4e src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Sun Nov 03 21:04:12 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sun Nov 03 21:12:50 2024 +0100
@@ -13,7 +13,7 @@
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.JScrollPane
 
-import org.gjt.sp.jedit.{View, OperatingSystem}
+import org.gjt.sp.jedit.View
 
 
 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) {
@@ -95,8 +95,8 @@
     tree.setVisibleRowCount(visible)
   }
 
-  private val tree_view = new JScrollPane(tree)
-  tree_view.setMinimumSize(new Dimension(200, 50))
+  private val tree_scroller = new JScrollPane(tree)
+  tree_scroller.setMinimumSize(new Dimension(200, 50))
 
-  set_content(tree_view)
+  set_content(tree_scroller)
 }