# HG changeset patch
# User wenzelm
# Date 1735306298 -3600
# Node ID 201ec2e401cb107f2dd30143c1fcafaf2ac2aa6a
# Parent  09c535d9ff0cec7ff010d22be7699075aa9b03a5
tuned, following theories_status.scala;

diff -r 09c535d9ff0c -r 201ec2e401cb src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 16:42:32 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 27 14:31:38 2024 +0100
@@ -28,43 +28,44 @@
         entry2.timing compare entry1.timing
     }
 
-    object Renderer_Component extends Label {
-      opaque = false
-      xAlignment = Alignment.Leading
-      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
+    class Renderer extends ListView.Renderer[Entry] {
+      private object component extends Label {
+        var entry: Entry = null
+
+        opaque = false
+        xAlignment = Alignment.Leading
+        border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
 
-      var entry: Entry = null
-      override def paintComponent(gfx: Graphics2D): Unit = {
-        def paint_rectangle(color: Color): Unit = {
-          val size = peer.getSize()
-          val insets = border.getBorderInsets(peer)
-          val x = insets.left
-          val y = insets.top
-          val w = size.width - x - insets.right
-          val h = size.height - y - insets.bottom
-          gfx.setColor(color)
-          gfx.fillRect(x, y, w, h)
-        }
+        override def paintComponent(gfx: Graphics2D): Unit = {
+          def paint_rectangle(color: Color): Unit = {
+            val size = peer.getSize()
+            val insets = border.getBorderInsets(peer)
+            val x = insets.left
+            val y = insets.top
+            val w = size.width - x - insets.right
+            val h = size.height - y - insets.bottom
+            gfx.setColor(color)
+            gfx.fillRect(x, y, w, h)
+          }
 
-        entry match {
-          case theory_entry: Theory_Entry if theory_entry.current =>
-            paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
-          case _: Command_Entry =>
-            paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
-          case _ =>
+          entry match {
+            case theory_entry: Theory_Entry if theory_entry.current =>
+              paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
+            case _: Command_Entry =>
+              paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
+            case _ =>
+          }
+          super.paintComponent(gfx)
         }
-        super.paintComponent(gfx)
       }
-    }
 
-    class Renderer extends ListView.Renderer[Entry] {
       def componentFor(
         list: ListView[_ <: Timing_Dockable.this.Entry],
         isSelected: Boolean,
         focused: Boolean,
-        entry: Entry, index: Int
+        entry: Entry,
+        index: Int
       ): Component = {
-        val component = Renderer_Component
         component.entry = entry
         component.text = entry.gui_text
         component