--- 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 \
--- 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"
--- 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)
}