# HG changeset patch
# User wenzelm
# Date 1708178693 -3600
# Node ID 1b0668acf319e1e9158f33bbd99efea4f84b5eb3
# Parent  bc6033faa22920137940f7d305df64b1833a6c65
clarified signature;

diff -r bc6033faa229 -r 1b0668acf319 etc/build.props
--- a/etc/build.props	Sat Feb 17 15:00:46 2024 +0100
+++ b/etc/build.props	Sat Feb 17 15:04:53 2024 +0100
@@ -320,7 +320,7 @@
 services = \
   isabelle.Bash$Handler \
   isabelle.Bibtex$File_Format \
-  isabelle.Build$Default_Engine \
+  isabelle.Build$Engine$Default \
   isabelle.Build_Schedule$Build_Engine \
   isabelle.Document_Build$Build_Engine \
   isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \
diff -r bc6033faa229 -r 1b0668acf319 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Feb 17 15:00:46 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Feb 17 15:04:53 2024 +0100
@@ -28,7 +28,7 @@
   sealed case class Context(
     store: Store,
     build_deps: isabelle.Sessions.Deps,
-    engine: Engine = Default_Engine,
+    engine: Engine = Engine.Default,
     afp_root: Option[Path] = None,
     build_hosts: List[Build_Cluster.Host] = Nil,
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
@@ -104,6 +104,9 @@
 
     def apply(name: String): Engine =
       services.find(_.name == name).getOrElse(error("Bad build engine " + quote(name)))
+
+    class Default extends Engine("") { override def toString: String = "<default>" }
+    object Default extends Default
   }
 
   class Engine(val name: String) extends Isabelle_System.Service {
@@ -141,8 +144,6 @@
     }
   }
 
-  class Default_Engine extends Engine("") { override def toString: String = "<default>" }
-  object Default_Engine extends Default_Engine
 
 
   /* build */
diff -r bc6033faa229 -r 1b0668acf319 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Sat Feb 17 15:00:46 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Sat Feb 17 15:04:53 2024 +0100
@@ -27,7 +27,7 @@
   def benchmark_requirements(options: Options, progress: Progress = new Progress): Unit = {
     val res =
       Build.build(
-        options.string.update("build_engine", Build.Default_Engine.name),
+        options.string.update("build_engine", Build.Engine.Default.name),
         selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)),
         progress = progress, build_heap = true)
     if (!res.ok) error("Failed building requirements")