# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701464255 -3600
# Node ID c1255d9870f6f86becc3801618d2495050f7d0a0
# Parent  ed00312f694fa75c8d3eaf677defb3b67c0e963f
clarified heuristics toString;
add generator description to schedule;

diff -r ed00312f694f -r c1255d9870f6 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:54:00 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 01 21:57:35 2023 +0100
@@ -422,13 +422,13 @@
     type Graph = isabelle.Graph[String, Node]
   }
 
-  case class Schedule(start: Date, graph: Schedule.Graph) {
+  case class Schedule(generator: String, start: Date, graph: Schedule.Graph) {
     def end: Date =
       if (graph.is_empty) start
       else graph.maximals.map(graph.get_node).map(_.end).maxBy(_.unix_epoch)
 
     def duration: Time = end.time - start.time
-    def message: String = "Estimated " + duration.message_hms + " build time"
+    def message: String = "Estimated " + duration.message_hms + " build time with " + generator
   }
 
   case class State(build_state: Build_Process.State, current_time: Time, finished: Schedule) {
@@ -485,7 +485,8 @@
         }
 
       val start = Date.now()
-      val end_state = simulate(State(build_state, start.time, Schedule(start, Graph.empty)))
+      val end_state =
+        simulate(State(build_state, start.time, Schedule(toString, start, Graph.empty)))
 
       end_state.finished
     }
@@ -493,6 +494,7 @@
 
   class Default_Heuristic(timing_data: Timing_Data, options: Options)
     extends Heuristic(timing_data) {
+    override def toString: String = "default build heuristic"
 
     def host_threads(host: Host): Int = {
       val m = (options ++ host.build.options).int("threads")
@@ -602,6 +604,7 @@
     sessions_structure: Sessions.Structure,
     max_threads_limit: Int = 8
   ) extends Path_Heuristic(timing_data, sessions_structure, max_threads_limit) {
+    override def toString: String = "path time heuristic (threshold: " + threshold.message_hms + ")"
 
     def next(state: Build_Process.State): List[Config] = {
       val resources = host_infos.available(state)