# HG changeset patch
# User wenzelm
# Date 1622842246 -7200
# Node ID b73777a0c076fcc48fff49b62815e81ad17955c9
# Parent  451fc6be6c5bc939c8b5e58dc43a1392b4642f43
allow build session setup, e.g. for protocol handlers;

diff -r 451fc6be6c5b -r b73777a0c076 src/Pure/Tools/build.scala
--- 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 {
diff -r 451fc6be6c5b -r b73777a0c076 src/Pure/Tools/build_job.scala
--- 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 =