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