# HG changeset patch
# User wenzelm
# Date 1730661312 -3600
# Node ID 2529568daaff000a001560751e178e64ac00e5ad
# Parent  403203217493e6f6fe1a32690ab882f76a07df05
tuned names;

diff -r 403203217493 -r 2529568daaff src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sun Nov 03 20:05:06 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sun Nov 03 20:15:12 2024 +0100
@@ -67,7 +67,7 @@
 
   /* pretty text area */
 
-  private val tree_text_area: Tree_Text_Area =
+  private val output: Tree_Text_Area =
     new Tree_Text_Area(view, root_name = "Threads") {
       override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
         update_focus()
@@ -95,17 +95,15 @@
     }
 
   override def detach_operation: Option[() => Unit] =
-    tree_text_area.pretty_text_area.detach_operation
+    output.pretty_text_area.detach_operation
 
-  tree_text_area.init_gui(dockable)
+  output.init_gui(dockable)
 
 
   /* tree view */
 
-  private def tree: Tree_View = tree_text_area.tree
-
   private def tree_selection(): Option[Debugger.Context] =
-    tree_text_area.tree.get_selection({ case c: Debugger.Context => c })
+    output.tree.get_selection({ case c: Debugger.Context => c })
 
   private def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
 
@@ -122,30 +120,30 @@
         case _ => thread_contexts.headOption
       }
 
-    tree_text_area.tree.clear()
+    output.tree.clear()
 
     for (thread <- thread_contexts) {
       val thread_node = new DefaultMutableTreeNode(thread)
       for ((_, i) <- thread.debug_states.zipWithIndex)
         thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
-      tree_text_area.tree.root.add(thread_node)
+      output.tree.root.add(thread_node)
     }
 
-    tree_text_area.tree.reload_model()
+    output.tree.reload_model()
 
-    tree.expandRow(0)
-    for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i)
+    output.tree.expandRow(0)
+    for (i <- Range.inclusive(output.tree.getRowCount - 1, 1, -1)) output.tree.expandRow(i)
 
     new_tree_selection match {
       case Some(c) =>
         val i =
           (for (t <- thread_contexts.iterator.takeWhile(t => c.thread_name != t.thread_name))
             yield t.size).sum
-        tree.addSelectionRow(i + c.index + 1)
+        output.tree.addSelectionRow(i + c.index + 1)
       case None =>
     }
 
-    tree.revalidate()
+    output.tree.revalidate()
   }
 
   def update_vals(): Unit = {
@@ -240,7 +238,7 @@
   }
 
   private val zoom =
-    new Font_Info.Zoom { override def changed(): Unit = tree_text_area.handle_resize() }
+    new Font_Info.Zoom { override def changed(): Unit = output.handle_resize() }
 
   private val controls =
     Wrap_Panel(
@@ -248,8 +246,8 @@
         break_button, continue_button, step_button, step_over_button, step_out_button,
         context_label, Component.wrap(context_field),
         expression_label, Component.wrap(expression_field), eval_button, sml_button,
-        tree_text_area.pretty_text_area.search_label,
-        tree_text_area.pretty_text_area.search_field, zoom))
+        output.pretty_text_area.search_label,
+        output.pretty_text_area.search_field, zoom))
 
   add(controls.peer, BorderLayout.NORTH)
 
@@ -275,12 +273,12 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        GUI_Thread.later { tree_text_area.handle_resize() }
+        GUI_Thread.later { output.handle_resize() }
 
       case Debugger.Update =>
         GUI_Thread.later {
           break_button.selected = debugger.is_break()
-          tree_text_area.handle_update()
+          output.handle_update()
         }
     }
 
@@ -288,14 +286,14 @@
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
     debugger.init(dockable)
-    tree_text_area.handle_update()
+    output.handle_update()
     jEdit.propertiesChanged()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
-    tree_text_area.delay_resize.revoke()
+    output.delay_resize.revoke()
     debugger.exit(dockable)
     jEdit.propertiesChanged()
   }