clarified signature;
authorwenzelm
Sat, 17 Feb 2024 15:04:53 +0100
changeset 79642 1b0668acf319
parent 79641 bc6033faa229
child 79643 51e9d1a80e39
clarified signature;
etc/build.props
src/Pure/Build/build.scala
src/Pure/Build/build_benchmark.scala
--- 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")