src/Tools/jEdit/src/info_dockable.scala

--- a/src/Tools/jEdit/src/info_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -76,7 +76,8 @@
   private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components)
   add(controls.peer, BorderLayout.NORTH)
 
-  output.init_gui(dockable, split = true)
+  output.setup(dockable)
+  set_content(output.split_pane)
 
 
   /* main */