# HG changeset patch
# User wenzelm
# Date 1678188105 -3600
# Node ID 4ad322ee6025f380baf8d672f5a74cdcbab40e8f
# Parent  2d06b514b3633b2ea22c9e305152c2c45218e192
clarified signature: support all arguments of Sessions.store();

diff -r 2d06b514b363 -r 4ad322ee6025 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 07 12:15:37 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 07 12:21:45 2023 +0100
@@ -69,13 +69,13 @@
   def hostname(options: Options): String =
     Isabelle_System.hostname(options.string("build_hostname"))
 
-  def build_init(options: Options): Sessions.Store = {
+  def build_init(options: Options, cache: Term.Cache = Term.Cache.make()): Sessions.Store = {
     val build_options =
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
         ("pide_reports=" + options.bool("build_pide_reports"))
-    val store = Sessions.store(build_options)
+    val store = Sessions.store(build_options, cache = cache)
 
     Isabelle_Fonts.init()
 
@@ -105,9 +105,10 @@
     soft_build: Boolean = false,
     export_files: Boolean = false,
     augment_options: String => List[Options.Spec] = _ => Nil,
-    session_setup: (String, Session) => Unit = (_, _) => ()
+    session_setup: (String, Session) => Unit = (_, _) => (),
+    cache: Term.Cache = Term.Cache.make()
   ): Results = {
-    val store = build_init(options)
+    val store = build_init(options, cache = cache)
     val build_options = store.options
 
 
@@ -388,9 +389,10 @@
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
-    session_setup: (String, Session) => Unit = (_, _) => ()
+    session_setup: (String, Session) => Unit = (_, _) => (),
+    cache: Term.Cache = Term.Cache.make()
   ): Results = {
-    val store = build_init(options)
+    val store = build_init(options, cache = cache)
     val build_options = store.options
 
     progress.echo("build worker for " + build_uuid)