tuned signature;
authorwenzelm
Thu, 26 Dec 2024 12:46:45 +0100
changeset 81653 18c16b94164a
parent 81652 4268b8f841e4
child 81654 f13d04506126
tuned signature;
src/Tools/jEdit/src/timing_dockable.scala
--- 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))
   }