tuned;

--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 12:12:37 2022 +0200
@@ -102,13 +102,13 @@
     }
 
   override def init(): Unit = {
-    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main
     handle_resize()
   }
 
   override def exit(): Unit = {
-    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main
     delay_resize.revoke()
   }