# HG changeset patch
# User wenzelm
# Date 1730979164 -3600
# Node ID 072ce947ee507eeecb09ef5464a7e1e46f850740
# Parent  6cb5ac3096fad2ab1f18ad11b9b8bf49c698c1b9
tuned signature: more standard names;

diff -r 6cb5ac3096fa -r 072ce947ee50 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 12:26:36 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 12:32:44 2024 +0100
@@ -53,7 +53,7 @@
         text_area.update(snapshot, Command.Results.empty, Nil)
     }
 
-    do_paint()
+    handle_resize()
   }
 
   private def show_trace(): Unit = {
@@ -61,14 +61,12 @@
     new Simplifier_Trace_Window(view, current_snapshot, trace)
   }
 
-  private def do_paint(): Unit = {
+  private def handle_resize(): Unit = {
     GUI_Thread.later {
       text_area.resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale")))
     }
   }
 
-  private def handle_resize(): Unit = do_paint()
-
   private def handle_update(follow: Boolean): Unit = {
     val (new_snapshot, new_command, new_results, new_id) =
       PIDE.editor.current_node_snapshot(view) match {
diff -r 6cb5ac3096fa -r 072ce947ee50 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 12:26:36 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 12:32:44 2024 +0100
@@ -133,7 +133,7 @@
   GUI_Thread.require {}
 
   private val pretty_text_area = new Pretty_Text_Area(view)
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = do_paint() }
+  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
 
   size = new Dimension(500, 500)
   contents = new BorderPanel {
@@ -149,20 +149,18 @@
       new Simplifier_Trace_Window.Root_Tree(0)
   }
 
-  do_update()
+  handle_update()
   open()
-  do_paint()
+  handle_resize()
 
-  def do_update(): Unit = {
+  def handle_update(): Unit = {
     val xml = tree.format
     pretty_text_area.update(snapshot, Command.Results.empty, xml)
   }
 
-  def do_paint(): Unit =
+  def handle_resize(): Unit =
     GUI_Thread.later { pretty_text_area.zoom(zoom) }
 
-  def handle_resize(): Unit = do_paint()
-
 
   /* resize */