# HG changeset patch
# User wenzelm
# Date 1730905650 -3600
# Node ID 969280db8ca5eafa4d11eeca00ca001afbf148ba
# Parent  1206400b9b4841a805cdac0525f666da0d4b26a4
clarified signature;

diff -r 1206400b9b48 -r 969280db8ca5 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 06 15:52:31 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 06 16:07:30 2024 +0100
@@ -67,7 +67,7 @@
   /* pretty text area */
 
   private val output: Output_Area =
-    new Output_Area(view, root_name = "Threads") {
+    new Output_Area(view, root_name = "Threads", split = true) {
       override def handle_resize(): Unit = pretty_text_area.zoom(zoom)
 
       override def handle_update(): Unit = {
diff -r 1206400b9b48 -r 969280db8ca5 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Wed Nov 06 15:52:31 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Wed Nov 06 16:07:30 2024 +0100
@@ -20,7 +20,10 @@
 import org.gjt.sp.jedit.View
 
 
-class Output_Area(view: View, root_name: String = "Overview") {
+class Output_Area(view: View,
+  root_name: String = "Overview",
+  split: Boolean = false
+) {
   GUI_Thread.require {}
 
 
@@ -41,18 +44,27 @@
     Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
 
 
-  /* main pane */
+  /* main GUI components */
+
+  lazy val tree_pane: Component = {
+    val scroll_pane: ScrollPane = new ScrollPane(Component.wrap(tree))
+    scroll_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+    scroll_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+    scroll_pane.minimumSize = new Dimension(200, 100)
+    scroll_pane
+  }
 
-  val tree_pane: ScrollPane = new ScrollPane(Component.wrap(tree))
-  tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
-  tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-  tree_pane.minimumSize = new Dimension(200, 100)
+  lazy val text_pane: Component = Component.wrap(pretty_text_area)
 
-  val main_pane: SplitPane = new SplitPane(Orientation.Vertical) {
-    oneTouchExpandable = true
-    leftComponent = tree_pane
-    rightComponent = Component.wrap(pretty_text_area)
-  }
+  lazy val main_pane: Component =
+    if (split) {
+      new SplitPane(Orientation.Vertical) {
+        oneTouchExpandable = true
+        leftComponent = tree_pane
+        rightComponent = text_pane
+      }
+    }
+    else text_pane
 
 
   /* GUI component */