# HG changeset patch
# User wenzelm
# Date 1732027582 -3600
# Node ID 07e79b80e96d12f58715e526ed7c82df7b9b93c1
# Parent  480dffe5741f2a56ceb3cde16851645db2035e0a
clarified signature: avoid implicit functionality;

diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -96,7 +96,8 @@
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
 
-  output.init_gui(dockable, split = true)
+  output.setup(dockable)
+  set_content(output.split_pane)
 
 
   /* tree view */
diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -347,7 +347,7 @@
 
   message_pane.pages ++= List(input_page, output_page)
 
-  output.init_gui(dockable, set_content = false)
+  output.setup(dockable)
   set_content(message_pane)
 
 
diff -r 480dffe5741f -r 07e79b80e96d 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 */
diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -113,16 +113,11 @@
       rightComponent = text_pane
     }
 
-  def init_gui(parent: JComponent, split: Boolean = false, set_content: Boolean = true): Unit = {
+  def setup(parent: JComponent): Unit = {
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
     tree.addTreeSelectionListener(tree_selection_listener)
-    parent match {
-      case dockable: Dockable if set_content =>
-        dockable.set_content(if (split) split_pane else text_pane)
-      case _ =>
-    }
   }
 
   def init(): Unit = {
diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -58,7 +58,8 @@
     }
   }
 
-  output.init_gui(dockable, split = true)
+  output.setup(dockable)
+  dockable.set_content(output.split_pane)
 
 
   /* controls */
diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -18,6 +18,8 @@
 
 
 class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
@@ -31,7 +33,9 @@
 
 
   private val output: Output_Area = new Output_Area(view)
-  output.init_gui(this)
+
+  output.setup(dockable)
+  set_content(output.text_pane)
 
   private def update_contents(): Unit = {
     val snapshot = current_snapshot
diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -19,6 +19,8 @@
 
 
 class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
@@ -28,7 +30,8 @@
 
   override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
 
-  output.init_gui(this)
+  output.setup(dockable)
+  set_content(output.text_pane)
 
 
   /* query operation */
diff -r 480dffe5741f -r 07e79b80e96d src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Tue Nov 19 15:35:03 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Tue Nov 19 15:46:22 2024 +0100
@@ -16,6 +16,8 @@
 
 
 class State_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
@@ -28,7 +30,8 @@
   private val print_state =
     new Query_Operation(PIDE.editor, view, "print_state", _ => (), output.pretty_text_area.update)
 
-  output.init_gui(this, split = true)
+  output.setup(dockable)
+  set_content(output.split_pane)
 
 
   /* update */