--- 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 \
--- 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 */
--- 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")