# HG changeset patch
# User wenzelm
# Date 1732026311 -3600
# Node ID 9b55af09cb1f17884d498f5e2157cebdc37230e2
# Parent  7293d47a9a70afd25bc34d792282a8838b6e0e32
re-use Output_Area;

diff -r 7293d47a9a70 -r 9b55af09cb1f src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Nov 19 10:52:02 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Nov 19 15:25:11 2024 +0100
@@ -65,13 +65,16 @@
   private val current_state = Synchronized(Document_Dockable.State.init())
 
   private val process_indicator = new Process_Indicator
-  private val pretty_text_area = new Pretty_Text_Area(view)
+  private val output: Output_Area = new Output_Area(view)
   private val message_pane = new TabbedPane
 
+  override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
+
+
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
-    pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all)
+    output.pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all)
 
     if (st.running) process_indicator.update("Running document build process ...", 15)
     else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5)
@@ -84,21 +87,6 @@
   }
 
 
-  /* text area with zoom/resize */
-
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
-  private val delay_resize: Delay =
-    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()
-  })
-
-
   /* progress */
 
   class Log_Progress extends Program_Progress(default_title = "build") {
@@ -348,16 +336,18 @@
       override def clicked(): Unit = cancel_process()
     }
 
-  private val output_controls = Wrap_Panel(List(cancel_button, pretty_text_area.zoom_component))
+  private val output_controls =
+    Wrap_Panel(List(cancel_button, output.pretty_text_area.zoom_component))
 
   private val output_page =
     new TabbedPane.Page("Output", new BorderPanel {
       layout(output_controls) = BorderPanel.Position.North
-      layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
+      layout(output.text_pane) = BorderPanel.Position.Center
     }, "Results from document build process")
 
   message_pane.pages ++= List(input_page, output_page)
 
+  output.init_gui(dockable, set_content = false)
   set_content(message_pane)
 
 
@@ -368,7 +358,7 @@
       case _: Session.Global_Options =>
         GUI_Thread.later {
           document_session.load()
-          handle_resize()
+          output.handle_resize()
           refresh_theories()
         }
       case changed: Session.Commands_Changed =>
@@ -397,14 +387,14 @@
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
-    handle_resize()
+    output.init()
     delay_load.invoke()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
-    delay_resize.revoke()
+    output.exit()
     PIDE.editor.document_exit(dockable)
   }
 }
diff -r 7293d47a9a70 -r 9b55af09cb1f src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 10:52:02 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 15:25:11 2024 +0100
@@ -113,13 +113,14 @@
       rightComponent = text_pane
     }
 
-  def init_gui(parent: JComponent, split: Boolean = false): Unit = {
+  def init_gui(parent: JComponent, split: Boolean = false, set_content: Boolean = true): Unit = {
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
     tree.addTreeSelectionListener(tree_selection_listener)
     parent match {
-      case dockable: Dockable => dockable.set_content(if (split) split_pane else text_pane)
+      case dockable: Dockable if set_content =>
+        dockable.set_content(if (split) split_pane else text_pane)
       case _ =>
     }
   }