# HG changeset patch
# User wenzelm
# Date 1731765881 -3600
# Node ID 6ea0055fa42da2efc47677e8797238152ed6428d
# Parent  570b4652d143586cd4caf5416df5a00f59fc7c7e
clarified signature;

diff -r 570b4652d143 -r 6ea0055fa42d src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Nov 15 23:25:18 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 16 15:04:41 2024 +0100
@@ -67,7 +67,7 @@
   /* pretty text area */
 
   private val output: Output_Area =
-    new Output_Area(view, root_name = "Threads", split = true) {
+    new Output_Area(view, root_name = "Threads") {
       override def handle_update(): Unit = {
         val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
         val (new_threads, new_output) = debugger.status(tree_selection())
@@ -89,7 +89,7 @@
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
 
-  output.init_gui(dockable)
+  output.init_gui(dockable, split = true)
 
 
   /* tree view */
diff -r 570b4652d143 -r 6ea0055fa42d src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Fri Nov 15 23:25:18 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Sat Nov 16 15:04:41 2024 +0100
@@ -20,10 +20,7 @@
 import org.gjt.sp.jedit.View
 
 
-class Output_Area(view: View,
-  root_name: String = "Overview",
-  split: Boolean = false
-) {
+class Output_Area(view: View, root_name: String = "Overview") {
   GUI_Thread.require {}
 
 
@@ -44,7 +41,36 @@
     Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
 
 
-  /* main GUI components */
+  /* handle events */
+
+  def handle_focus(): Unit = ()
+
+  private lazy val component_listener =
+    new ComponentAdapter {
+      override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+      override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+    }
+
+  private lazy val focus_listener =
+    new FocusAdapter {
+      override def focusGained(e: FocusEvent): Unit = handle_focus()
+    }
+
+  private lazy val mouse_listener =
+    new MouseAdapter {
+      override def mouseClicked(e: MouseEvent): Unit = {
+        if (!e.isConsumed()) {
+          val click = tree.getPathForLocation(e.getX, e.getY)
+          if (click != null && e.getClickCount == 1) {
+            e.consume()
+            handle_focus()
+          }
+        }
+      }
+    }
+
+
+  /* GUI components */
 
   lazy val tree_pane: Component = {
     val scroll_pane: ScrollPane = new ScrollPane(Component.wrap(tree))
@@ -56,47 +82,19 @@
 
   lazy val text_pane: Component = Component.wrap(pretty_text_area)
 
-  lazy val main_pane: Component =
-    if (split) {
-      new SplitPane(Orientation.Vertical) {
-        oneTouchExpandable = true
-        leftComponent = tree_pane
-        rightComponent = text_pane
-      }
+  lazy val split_pane: SplitPane =
+    new SplitPane(Orientation.Vertical) {
+      oneTouchExpandable = true
+      leftComponent = tree_pane
+      rightComponent = text_pane
     }
-    else text_pane
-
-
-  /* GUI component */
-
-  def handle_focus(): Unit = ()
 
-  def init_gui(parent: JComponent): Unit = {
-    parent.addComponentListener(
-      new ComponentAdapter {
-        override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-        override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-      })
-    parent.addFocusListener(
-      new FocusAdapter {
-        override def focusGained(e: FocusEvent): Unit = handle_focus()
-      })
-
-    tree.addMouseListener(
-      new MouseAdapter {
-        override def mouseClicked(e: MouseEvent): Unit = {
-          if (!e.isConsumed()) {
-            val click = tree.getPathForLocation(e.getX, e.getY)
-            if (click != null && e.getClickCount == 1) {
-              e.consume()
-              handle_focus()
-            }
-          }
-        }
-      })
-
+  def init_gui(parent: JComponent, split: Boolean = false): Unit = {
+    parent.addComponentListener(component_listener)
+    parent.addFocusListener(focus_listener)
+    tree.addMouseListener(mouse_listener)
     parent match {
-      case dockable: Dockable => dockable.set_content(main_pane)
+      case dockable: Dockable => dockable.set_content(if (split) split_pane else text_pane)
       case _ =>
     }
   }