# HG changeset patch
# User wenzelm
# Date 1735226188 -3600
# Node ID 98ecc0ed6af1a126524e9ee1be5143008eab8ca7
# Parent  56ad9ddc283af6b3cccfea0ae96e552a9ebffda7
clarified signature: ensure uniform style;

diff -r 56ad9ddc283a -r 98ecc0ed6af1 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Dec 26 15:43:07 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Dec 26 16:16:28 2024 +0100
@@ -116,6 +116,8 @@
     prefix: String = "",
     style: Style = Style_Plain
   ) {
+    def set_style(new_style: Style): Name = copy(style = new_style)
+
     override def toString: String = {
       val a = kind.nonEmpty
       val b = name.nonEmpty
diff -r 56ad9ddc283a -r 98ecc0ed6af1 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 15:43:07 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 16:16:28 2024 +0100
@@ -77,11 +77,10 @@
     def timing: Double
     def gui_name: GUI.Name
     def gui_text: String = {
-      val name = gui_name
-      val style = name.style
+      val style = GUI.Style_HTML
       style.enclose(
         style.spaces(2 * depth) + style.make_text(Time.print_seconds(timing) + "s ") +
-        name.toString)
+        gui_name.set_style(style).toString)
     }
     def follow(snapshot: Document.Snapshot): Unit
   }
@@ -89,7 +88,7 @@
   private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
   extends Entry {
     def make_current: Theory_Entry = copy(current = true)
-    def gui_name: GUI.Name = GUI.Name(name.theory, kind = "theory", style = GUI.Style_HTML)
+    def gui_name: GUI.Name = GUI.Name(name.theory, kind = "theory")
     def follow(snapshot: Document.Snapshot): Unit =
       PIDE.editor.goto_file(true, view, name.node)
   }
@@ -97,7 +96,7 @@
   private case class Command_Entry(command: Command, timing: Double)
   extends Entry {
     override def depth: Int = 1
-    def gui_name: GUI.Name = GUI.Name(command.span.name, kind = "command", style = GUI.Style_HTML)
+    def gui_name: GUI.Name = GUI.Name(command.span.name, kind = "command")
     def follow(snapshot: Document.Snapshot): Unit =
       PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view))
   }