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