diff -r a00d4d50b851 -r 5f28bded8d7d src/Tools/jEdit/src/tree_text_area.scala
--- 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