src/Pure/Build/build_job.scala
changeset 83287 24000abcefab
parent 83262 9fe2fedc9842
child 83295 094d96f05cba
--- a/src/Pure/Build/build_job.scala	Wed Oct 15 16:31:05 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Wed Oct 15 21:53:16 2025 +0200
@@ -219,12 +219,6 @@
       nodes_changed += state_id
       nodes_delay.invoke()
     }
-
-    def get_theory_timings(): List[Properties.T] = synchronized {
-      nodes_domain.map(name =>
-        Markup.Name(name.theory) :::
-        Markup.Timing_Properties(nodes_status(name).total_timing))
-    }
   }
 
   class Session_Job private[Build_Job](