--- 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
--- 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))
}