# HG changeset patch
# User wenzelm
# Date 1708178374 -3600
# Node ID 7a2b86a48be0b6316a31cdd50beedb84c0cf6b73
# Parent  8b8591820bd819d01a60787e3bd1b1f4bca0e594
prefer static object, while class is required for "services";

diff -r 8b8591820bd8 -r 7a2b86a48be0 etc/build.props
--- a/etc/build.props	Sat Feb 17 14:48:32 2024 +0100
+++ b/etc/build.props	Sat Feb 17 14:59:34 2024 +0100
@@ -321,7 +321,7 @@
   isabelle.Bash$Handler \
   isabelle.Bibtex$File_Format \
   isabelle.Build$Default_Engine \
-  isabelle.Build_Schedule$Engine \
+  isabelle.Build_Schedule$Build_Engine \
   isabelle.Document_Build$Build_Engine \
   isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \
   isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \
diff -r 8b8591820bd8 -r 7a2b86a48be0 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Feb 17 14:48:32 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Feb 17 14:59:34 2024 +0100
@@ -1216,8 +1216,7 @@
   }
 
 
-  class Engine extends Build.Engine("build_schedule") {
-
+  class Build_Engine extends Build.Engine("build_schedule") {
     def scheduler(timing_data: Timing_Data, context: Build.Context): Scheduler = {
       val sessions_structure = context.sessions_structure
 
@@ -1263,6 +1262,7 @@
         def init_scheduler(timing_data: Timing_Data): Scheduler = scheduler(timing_data, context)
       }
   }
+  object Build_Engine extends Build_Engine
 
 
   /* build schedule */
@@ -1281,10 +1281,8 @@
     session_setup: (String, Session) => Unit = (_, _) => (),
     cache: Term.Cache = Term.Cache.make()
   ): Schedule = {
-    val build_engine = new Engine
-
     val store =
-      build_engine.build_store(options, build_cluster = build_hosts.nonEmpty, cache = cache)
+      Build_Engine.build_store(options, build_cluster = build_hosts.nonEmpty, cache = cache)
     val log_store = Build_Log.store(options, cache = cache)
     val build_options = store.options
 
@@ -1304,7 +1302,7 @@
           inlined_files = true).check_errors
 
       val build_context =
-        Build.Context(store, build_deps, engine = build_engine, afp_root = afp_root,
+        Build.Context(store, build_deps, engine = Build_Engine, afp_root = afp_root,
           build_hosts = build_hosts, hostname = Build.hostname(build_options),
           numa_shuffling = numa_shuffling, max_jobs = Some(0), session_setup = session_setup,
           master = true)
@@ -1327,7 +1325,7 @@
       val build_state =
         Build_Process.State(sessions = sessions, pending = sessions.iterator.map(task).toList)
 
-      val scheduler = build_engine.scheduler(timing_data, build_context)
+      val scheduler = Build_Engine.scheduler(timing_data, build_context)
       def schedule_msg(res: Exn.Result[Schedule]): String =
         res match { case Exn.Res(schedule) => schedule.message case _ => "" }