# HG changeset patch
# User wenzelm
# Date 1676977432 -3600
# Node ID 47eb96592aa2196098bd155625830f121efb2cd7
# Parent  1b7c5d4b97a88355fb08460ed1581478ed6df0f8
support alternative build engines, via system option "build_engine";

diff -r 1b7c5d4b97a8 -r 47eb96592aa2 etc/build.props
--- a/etc/build.props	Tue Feb 21 11:20:42 2023 +0100
+++ b/etc/build.props	Tue Feb 21 12:03:52 2023 +0100
@@ -306,6 +306,7 @@
 services = \
   isabelle.Bash$Handler \
   isabelle.Bibtex$File_Format \
+  isabelle.Build$Default_Engine \
   isabelle.Document_Build$Build_Engine \
   isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \
   isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \
diff -r 1b7c5d4b97a8 -r 47eb96592aa2 etc/options
--- a/etc/options	Tue Feb 21 11:20:42 2023 +0100
+++ b/etc/options	Tue Feb 21 12:03:52 2023 +0100
@@ -172,7 +172,7 @@
   -- "ML process command prefix (process policy)"
 
 
-section "PIDE Build"
+section "Build Process"
 
 option pide_reports : bool = true
   -- "report PIDE markup (in ML)"
@@ -180,6 +180,9 @@
 option build_pide_reports : bool = true
   -- "report PIDE markup (in batch build)"
 
+option build_engine : string = ""
+  -- "alternative session build engine"
+
 
 section "Editor Session"
 
diff -r 1b7c5d4b97a8 -r 47eb96592aa2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Feb 21 11:20:42 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Feb 21 12:03:52 2023 +0100
@@ -9,7 +9,7 @@
 
 
 object Build {
-  /** build with results **/
+  /* results */
 
   object Results {
     def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results =
@@ -41,6 +41,29 @@
     override def toString: String = rc.toString
   }
 
+
+  /* engine */
+
+  abstract class Engine(val name: String) extends Isabelle_System.Service {
+    override def toString: String = name
+    def init(build_context: Build_Process.Context): Build_Process
+  }
+
+  class Default_Engine extends Engine("") {
+    override def toString: String = "<default>"
+    override def init(build_context: Build_Process.Context): Build_Process =
+      new Build_Process(build_context)
+  }
+
+  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)))
+
+
+  /* build */
+
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
@@ -147,7 +170,8 @@
 
     val results =
       Isabelle_Thread.uninterruptible {
-        val build_process = new Build_Process(build_context)
+        val engine = get_engine(build_options.string("build_engine"))
+        val build_process = engine.init(build_context)
         val res = build_process.run()
         Results(build_context, res)
       }