# HG changeset patch
# User wenzelm
# Date 1735213605 -3600
# Node ID 18c16b94164a0bd6eaa4d4dd3d840667dd2a8c21
# Parent  4268b8f841e458107769934eb313d69dca1659ef
tuned signature;

diff -r 4268b8f841e4 -r 18c16b94164a 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))
   }