# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1703006915 -3600
# Node ID 1f694e4b2b3aded81fbdb4a145676eb5ac2fffb2
# Parent  fb86fa1c6af953900c488f8498904cd946be6bc0
clarified signature;

diff -r fb86fa1c6af9 -r 1f694e4b2b3a src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Tue Dec 19 17:26:15 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Tue Dec 19 18:28:35 2023 +0100
@@ -459,8 +459,9 @@
 
     def num_built(state: Build_Process.State): Int = graph.keys.count(state.results.contains)
     def elapsed(): Time = Time.now() - start.time
+    def is_empty: Boolean = graph.is_empty
     def is_outdated(options: Options, state: Build_Process.State): Boolean =
-      if (graph.is_empty) true
+      if (is_empty) true
       else {
         num_built(state) > options.int("build_schedule_outdated_limit") &&
           elapsed() > options.seconds("build_schedule_outdated_delay")
@@ -1016,7 +1017,7 @@
 
           val new_schedule = scheduler.build_schedule(state).update(state)
           val schedule =
-            if (_schedule.graph.is_empty) new_schedule
+            if (_schedule.is_empty) new_schedule
             else List(_schedule.update(state), new_schedule).minBy(_.end)(Date.Ordering)
 
           val elapsed = Time.now() - start
@@ -1567,7 +1568,7 @@
           numa_shuffling = isabelle.Host.numa_check(progress, numa_shuffling),
           build_hosts = build_hosts.toList)
 
-      if (!schedule.graph.is_empty && output_file.nonEmpty)
+      if (!schedule.is_empty && output_file.nonEmpty)
         write_schedule_graphic(schedule, output_file.get)
     })
 }