# 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)