allow build session setup, e.g. for protocol handlers;
--- a/src/Pure/Tools/build.scala Fri Jun 04 22:58:38 2021 +0200
+++ b/src/Pure/Tools/build.scala Fri Jun 04 23:30:46 2021 +0200
@@ -183,7 +183,8 @@
no_build: Boolean = false,
soft_build: Boolean = false,
verbose: Boolean = false,
- export_files: Boolean = false): Results =
+ export_files: Boolean = false,
+ session_setup: (String, Session) => Unit = (_, _) => ()): Results =
{
val build_options =
options +
@@ -425,7 +426,7 @@
val numa_node = numa_nodes.next(used_node)
val job =
new Build_Job(progress, session_name, info, deps, store, do_store,
- log, numa_node, queue.command_timings(session_name))
+ log, session_setup, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
else {
--- a/src/Pure/Tools/build_job.scala Fri Jun 04 22:58:38 2021 +0200
+++ b/src/Pure/Tools/build_job.scala Fri Jun 04 23:30:46 2021 +0200
@@ -203,6 +203,7 @@
store: Sessions.Store,
do_store: Boolean,
log: Logger,
+ session_setup: (String, Session) => Unit,
val numa_node: Option[Int],
command_timings0: List[Properties.T])
{
@@ -410,6 +411,8 @@
case _ =>
}
+ session_setup(session_name, session)
+
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =