# HG changeset patch
# User wenzelm
# Date 1688129798 -7200
# Node ID 45c7b88d160940562842807118ad3a522fe6840a
# Parent  3e8d443b95127e4de8246e46ee75febb06064167
clarified signature;

diff -r 3e8d443b9512 -r 45c7b88d1609 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jun 30 13:12:10 2023 +0200
+++ b/src/Pure/Tools/build.scala	Fri Jun 30 14:56:38 2023 +0200
@@ -14,6 +14,15 @@
 object Build {
   /** "isabelle build" **/
 
+  /* options */
+
+  def hostname(options: Options): String =
+    Isabelle_System.hostname(options.string("build_hostname"))
+
+  def engine_name(options: Options): String = options.string("build_engine")
+
+
+
   /* results */
 
   object Results {
@@ -49,46 +58,42 @@
 
   /* engine */
 
+  object Engine {
+    lazy val services: List[Engine] =
+      Isabelle_System.make_services(classOf[Engine])
+
+    def apply(name: String): Engine =
+      services.find(_.name == name).getOrElse(error("Bad build engine " + quote(name)))
+  }
+
   class Engine(val name: String) extends Isabelle_System.Service {
     override def toString: String = name
-    def init(build_context: Build_Process.Context, build_progress: Progress): Build_Process =
+
+    def build_options(options: Options): Options =
+      options + "completion_limit=0" + "editor_tracing_messages=0"
+
+    def build_process(build_context: Build_Process.Context, build_progress: Progress): Build_Process =
       new Build_Process(build_context, build_progress)
+
+    final def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store = {
+      val store = Store(build_options(options), cache = cache)
+      Isabelle_Fonts.init()
+      store
+    }
+
+    final def run(context: Build_Process.Context, progress: Progress): Results =
+      Isabelle_Thread.uninterruptible {
+        using(build_process(context, progress)) { build_process =>
+          Results(context, build_process.run())
+        }
+      }
   }
 
   class Default_Engine extends Engine("") { override def toString: String = "<default>" }
 
-  lazy val engines: List[Engine] =
-    Isabelle_System.make_services(classOf[Engine])
-
-  def get_engine(name: String): Engine =
-    engines.find(_.name == name).getOrElse(error("Bad build engine " + quote(name)))
-
-
-  /* options */
-
-  def hostname(options: Options): String =
-    Isabelle_System.hostname(options.string("build_hostname"))
-
-  def build_init(options: Options, cache: Term.Cache = Term.Cache.make()): Store = {
-    val build_options = options + "completion_limit=0" + "editor_tracing_messages=0"
-    val store = Store(build_options, cache = cache)
-
-    Isabelle_Fonts.init()
-
-    store
-  }
-
 
   /* build */
 
-  def build_results(options: Options, context: Build_Process.Context, progress: Progress): Results =
-    Isabelle_Thread.uninterruptible {
-      val engine = get_engine(options.string("build_engine"))
-      using(engine.init(context, progress)) { build_process =>
-        Results(context, build_process.run())
-      }
-    }
-
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
@@ -112,7 +117,9 @@
     session_setup: (String, Session) => Unit = (_, _) => (),
     cache: Term.Cache = Term.Cache.make()
   ): Results = {
-    val store = build_init(options, cache = cache)
+    val build_engine = Engine(engine_name(options))
+
+    val store = build_engine.store(options, cache = cache)
     val build_options = store.options
 
 
@@ -188,7 +195,7 @@
       }
     }
 
-    val results = build_results(build_options, build_context, progress)
+    val results = build_engine.run(build_context, progress)
 
     if (export_files) {
       for (name <- full_sessions_selection.iterator if results(name).ok) {
@@ -429,7 +436,9 @@
     max_jobs: Int = 1,
     cache: Term.Cache = Term.Cache.make()
   ): Results = {
-    val store = build_init(options, cache = cache)
+    val build_engine = Engine(engine_name(options))
+
+    val store = build_engine.store(options, cache = cache)
     val build_options = store.options
 
     val sessions_structure =
@@ -444,7 +453,7 @@
         hostname = hostname(build_options), numa_shuffling = numa_shuffling, max_jobs = max_jobs,
         build_uuid = build_master.build_uuid)
 
-    build_results(build_options, build_context, progress)
+    build_engine.run(build_context, progress)
   }