# HG changeset patch
# User wenzelm
# Date 1735224187 -3600
# Node ID 56ad9ddc283af6b3cccfea0ae96e552a9ebffda7
# Parent  a904fcbbbdbc41e5443fca5cc15d95a33ce9ffd8
tuned GUI output;

diff -r a904fcbbbdbc -r 56ad9ddc283a src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 15:38:57 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 15:43:07 2024 +0100
@@ -66,31 +66,38 @@
       ): Component = {
         val component = Renderer_Component
         component.entry = entry
-        component.text = entry.print
+        component.text = entry.gui_text
         component
       }
     }
   }
 
   private abstract class Entry {
+    def depth: Int = 0
     def timing: Double
-    def print: String
+    def gui_name: GUI.Name
+    def gui_text: String = {
+      val name = gui_name
+      val style = name.style
+      style.enclose(
+        style.spaces(2 * depth) + style.make_text(Time.print_seconds(timing) + "s ") +
+        name.toString)
+    }
     def follow(snapshot: Document.Snapshot): Unit
   }
 
   private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
   extends Entry {
     def make_current: Theory_Entry = copy(current = true)
-    def print: String =
-      Time.print_seconds(timing) + "s theory " + quote(name.theory)
+    def gui_name: GUI.Name = GUI.Name(name.theory, kind = "theory", style = GUI.Style_HTML)
     def follow(snapshot: Document.Snapshot): Unit =
       PIDE.editor.goto_file(true, view, name.node)
   }
 
   private case class Command_Entry(command: Command, timing: Double)
   extends Entry {
-    def print: String =
-      "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
+    override def depth: Int = 1
+    def gui_name: GUI.Name = GUI.Name(command.span.name, kind = "command", style = GUI.Style_HTML)
     def follow(snapshot: Document.Snapshot): Unit =
       PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view))
   }