# HG changeset patch
# User wenzelm
# Date 1732026898 -3600
# Node ID c7a88aaa60d20ee1baead5e54da1f2d39fe7106b
# Parent  9b55af09cb1f17884d498f5e2157cebdc37230e2
re-use Output_Area;

diff -r 9b55af09cb1f -r c7a88aaa60d2 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Nov 19 15:25:11 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Nov 19 15:34:58 2024 +0100
@@ -30,8 +30,8 @@
   private var do_update = true
 
 
-  private val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  private val output: Output_Area = new Output_Area(view)
+  output.init_gui(this)
 
   private def update_contents(): Unit = {
     val snapshot = current_snapshot
@@ -41,8 +41,8 @@
     context.questions.values.toList match {
       case q :: _ =>
         val data = q.data
-        val output = List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0))
-        pretty_text_area.update(snapshot, Command.Results.empty, output)
+        output.pretty_text_area.update(snapshot, Command.Results.empty,
+          List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0)))
         q.answers.foreach { answer =>
           answers.contents += new GUI.Button(answer.string) {
             override def clicked(): Unit =
@@ -50,10 +50,10 @@
           }
         }
       case Nil =>
-        pretty_text_area.update(snapshot, Command.Results.empty, Nil)
+        output.pretty_text_area.update(snapshot, Command.Results.empty, Nil)
     }
 
-    handle_resize()
+    output.handle_resize()
   }
 
   private def show_trace(): Unit = {
@@ -61,8 +61,6 @@
     new Simplifier_Trace_Window(view, current_snapshot, trace)
   }
 
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
   private def handle_update(follow: Boolean): Unit = {
     val (new_snapshot, new_command, new_results, new_id) =
       PIDE.editor.current_node_snapshot(view) match {
@@ -92,7 +90,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        GUI_Thread.later { handle_resize() }
+        GUI_Thread.later { output.handle_resize() }
 
       case changed: Session.Commands_Changed =>
         GUI_Thread.later { handle_update(do_update) }
@@ -109,6 +107,7 @@
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
     PIDE.session.trace_events += main
+    output.init()
     handle_update(true)
   }
 
@@ -117,21 +116,10 @@
     PIDE.session.commands_changed -= main
     PIDE.session.caret_focus -= main
     PIDE.session.trace_events -= main
-    delay_resize.revoke()
+    output.exit()
   }
 
 
-  /* 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()
-  })
-
-
   /* controls */
 
   private val controls =