--- a/src/Tools/jEdit/src/tree_text_area.scala Sat Nov 02 15:35:43 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala Sat Nov 02 15:42:37 2024 +0100
@@ -77,6 +77,11 @@
/* main pane */
+ def handle_focus(): Unit = ()
+
+ lazy val component_focus: FocusAdapter =
+ new FocusAdapter { override def focusGained(e: FocusEvent): Unit = handle_focus() }
+
val tree_pane: ScrollPane = new ScrollPane(Component.wrap(tree))
tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always