# HG changeset patch
# User wenzelm
# Date 1731869950 -3600
# Node ID 97a32b4d29e51a81a8971fcc5a557b8390c3651a
# Parent  eaf5c460ceb585981bbd623ab03bc00c94d4dfc8
clarified signature and modules: without GUI change yet;

diff -r eaf5c460ceb5 -r 97a32b4d29e5 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 17 19:49:25 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 17 19:59:10 2024 +0100
@@ -16,6 +16,9 @@
 
 
 class Output_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
+
   /* component state -- owned by GUI thread */
 
   private var do_update = true
@@ -24,15 +27,15 @@
 
   /* pretty text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
-
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+  private val output: Output_Area =
+    new Output_Area(view) {
+      override def handle_update(): Unit = dockable.handle_update(true)
+    }
 
+  override def detach_operation: Option[() => Unit] =
+    output.pretty_text_area.detach_operation
 
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
-  private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
+  private def handle_update(follow: Boolean, restriction: Option[Set[Command]] = None): Unit = {
     GUI_Thread.require {}
 
     for {
@@ -51,12 +54,14 @@
         else current_output
 
       if (current_output != new_output) {
-        pretty_text_area.update(snapshot, results, new_output)
+        output.pretty_text_area.update(snapshot, results, new_output)
         current_output = new_output
       }
     }
   }
 
+  output.init_gui(dockable)
+
 
   /* controls */
 
@@ -68,19 +73,19 @@
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
       do_update = state
-      handle_update(do_update, None)
+      handle_update(do_update)
     }
   }
 
   private val update_button = new GUI.Button("Update") {
     tooltip = "Update display according to the command at cursor position"
-    override def clicked(): Unit = handle_update(true, None)
+    override def clicked(): Unit = handle_update(true)
   }
 
   private val controls =
     Wrap_Panel(
       List(output_state_button, auto_hovering_button, auto_update_button, update_button) :::
-      pretty_text_area.search_zoom_components)
+      output.pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
@@ -91,42 +96,31 @@
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later {
-          handle_resize()
+          output.handle_resize()
           output_state_button.load()
           auto_hovering_button.load()
-          handle_update(do_update, None)
+          handle_update(do_update)
         }
 
       case changed: Session.Commands_Changed =>
         val restriction = if (changed.assignment) None else Some(changed.commands)
-        GUI_Thread.later { handle_update(do_update, restriction) }
+        GUI_Thread.later { handle_update(do_update, restriction = restriction) }
 
       case Session.Caret_Focus =>
-        GUI_Thread.later { handle_update(do_update, None) }
+        GUI_Thread.later { handle_update(do_update) }
     }
 
   override def init(): Unit = {
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
-    handle_update(true, None)
+    handle_update(true)
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     PIDE.session.caret_focus -= main
-    delay_resize.revoke()
+    output.delay_resize.revoke()
   }
-
-
-  /* resize */
-
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
 }