# HG changeset patch # User wenzelm # Date 1707997072 -3600 # Node ID 50376abd132dbebd74c7881f30dd8d4be85858a4 # Parent cdb51c7225ad30371d78bf945d06295e199ab860 tuned: prefer explicit update operation for immutable options; diff -r cdb51c7225ad -r 50376abd132d src/Pure/Build/build_schedule.scala --- a/src/Pure/Build/build_schedule.scala Thu Feb 15 12:18:25 2024 +0100 +++ b/src/Pure/Build/build_schedule.scala Thu Feb 15 12:37:52 2024 +0100 @@ -1038,7 +1038,7 @@ Benchmark.benchmark_requirements(build_options) if (build_context.jobs > 0) { - val benchmark_options = build_options.string("build_hostname") = hostname + val benchmark_options = build_options.string.update("build_hostname", hostname) Benchmark.benchmark(benchmark_options, progress) } _build_cluster.benchmark() diff -r cdb51c7225ad -r 50376abd132d src/Pure/System/benchmark.scala --- a/src/Pure/System/benchmark.scala Thu Feb 15 12:18:25 2024 +0100 +++ b/src/Pure/System/benchmark.scala Thu Feb 15 12:37:52 2024 +0100 @@ -25,7 +25,7 @@ def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = { val res = Build.build( - options.string("build_engine") = Build.Default_Engine().name, + options.string.update("build_engine", Build.Default_Engine().name), selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)), progress = progress, build_heap = true) if (!res.ok) error("Failed building requirements") @@ -41,7 +41,7 @@ progress.echo("Starting benchmark ...") val selection = Sessions.Selection(sessions = List(benchmark_session)) - val full_sessions = Sessions.load_structure(options.int("threads") = 1) + val full_sessions = Sessions.load_structure(options.int.update("threads", 1)) val build_context = Build.Context(store, new Build.Default_Engine, diff -r cdb51c7225ad -r 50376abd132d src/Pure/System/host.scala --- a/src/Pure/System/host.scala Thu Feb 15 12:18:25 2024 +0100 +++ b/src/Pure/System/host.scala Thu Feb 15 12:37:52 2024 +0100 @@ -62,22 +62,22 @@ numa_node match { case None => options case Some(node) => - options.string("process_policy") = if (numactl_ok(node)) numactl(node) else "" + options.string.update("process_policy", if (numactl_ok(node)) numactl(node) else "") } def node_options(options: Options, node: Node_Info): Options = { val threads_options = - if (node.rel_cpus.isEmpty) options else options.int("threads") = node.rel_cpus.length + if (node.rel_cpus.isEmpty) options else options.int.update("threads", node.rel_cpus.length) node.numa_node match { case None if node.rel_cpus.isEmpty => threads_options case Some(numa_node) => - threads_options.string("process_policy") = - if (numactl_ok(numa_node, node.rel_cpus)) numactl(numa_node, node.rel_cpus) else "" + threads_options.string.update("process_policy", + if (numactl_ok(numa_node, node.rel_cpus)) numactl(numa_node, node.rel_cpus) else "") case _ => - threads_options.string("process_policy") = - if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else "" + threads_options.string.update("process_policy", + if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else "") } } diff -r cdb51c7225ad -r 50376abd132d src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Thu Feb 15 12:18:25 2024 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Thu Feb 15 12:37:52 2024 +0100 @@ -288,7 +288,7 @@ } } - val session_options = options.bool("editor_output_state") = true + val session_options = options.bool.update("editor_output_state", true) val session = new Session(session_options, resources) Some((session_background, session))