--- 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