--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Dec 26 12:38:25 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Dec 26 12:46:45 2024 +0100
@@ -80,6 +80,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 print: String =
Time.print_seconds(timing) + "s theory " + quote(name.theory)
def follow(snapshot: Document.Snapshot): Unit =
@@ -163,7 +164,7 @@
yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
theories.flatMap(entry =>
- if (entry.name == name) entry.copy(current = true) :: commands
+ if (entry.name == name) entry.make_current :: commands
else List(entry))
}