--- 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 */