# HG changeset patch
# User wenzelm
# Date 1678125528 -3600
# Node ID 1d8a12d1c2e934e08cc6a507edc380fb92d9547e
# Parent  9b9179cda1551e91c9f0fe5100eceaca7b8a11c1
clarified signature;

diff -r 9b9179cda155 -r 1d8a12d1c2e9 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Mon Mar 06 17:29:00 2023 +0100
+++ b/src/Pure/System/host.scala	Mon Mar 06 18:58:48 2023 +0100
@@ -52,15 +52,14 @@
   def numactl(node: Int): String = "numactl -m" + node + " -N" + node
   def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok
 
-  def process_policy(node: Int): String = if (numactl_ok(node)) numactl(node) else ""
-
-  def process_policy_options(options: Options, numa_node: Option[Int]): Options =
+  def process_policy(options: Options, numa_node: Option[Int]): Options =
     numa_node match {
       case None => options
-      case Some(n) => options.string("process_policy") = process_policy(n)
+      case Some(node) =>
+        options.string("process_policy") = if (numactl_ok(node)) numactl(node) else ""
     }
 
-  def perhaps_process_policy_options(options: Options): Options = {
+  def perhaps_process_policy(options: Options): Options = {
     val numa_node =
       try {
         numa_nodes() match {
@@ -69,7 +68,7 @@
         }
       }
       catch { case ERROR(_) => None }
-    process_policy_options(options, numa_node)
+    process_policy(options, numa_node)
   }
 
 
diff -r 9b9179cda155 -r 1d8a12d1c2e9 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Mar 06 17:29:00 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Mar 06 18:58:48 2023 +0100
@@ -119,7 +119,7 @@
     def job_name: String = session_name
 
     private val info: Sessions.Info = session_background.sessions_structure(session_name)
-    private val options: Options = Host.process_policy_options(info.options, node_info.numa_node)
+    private val options: Options = Host.process_policy(info.options, node_info.numa_node)
 
     private val session_sources =
       Sessions.Sources.load(session_background.base, cache = store.cache.compress)
diff -r 9b9179cda155 -r 1d8a12d1c2e9 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Mar 06 17:29:00 2023 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Mar 06 18:58:48 2023 +0100
@@ -98,7 +98,7 @@
     ): Context = {
       val session_options: Options = {
         val options1 =
-          Host.perhaps_process_policy_options(options) +
+          Host.perhaps_process_policy(options) +
             "parallel_proofs=0" +
             "completion_limit=0" +
             "editor_tracing_messages=0"