src/Tools/jEdit/src/output_dockable.scala
changeset 81615 ebf954ceb4d1
parent 81493 07e79b80e96d
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Dec 16 22:53:31 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Dec 17 12:36:37 2024 +0100
@@ -27,8 +27,11 @@
 
   /* output area */
 
-  private val output: Output_Area =
-    new Output_Area(view) { override def handle_update(): Unit = dockable.handle_update(true) }
+  val output: Output_Area =
+    new Output_Area(view) {
+      override def handle_update(): Unit = dockable.handle_update(true)
+      override def handle_shown(): Unit = split_pane_layout()
+    }
 
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation