misc tuning and clarification;
support SSH.System;

--- a/src/Pure/System/numa.scala	Tue Feb 21 11:19:39 2023 +0100
+++ b/src/Pure/System/numa.scala	Tue Feb 21 11:20:42 2023 +0100
@@ -8,25 +8,28 @@
 
 
 object NUMA {
-  /* available nodes */
+  /* information about nodes */
 
-  def nodes(): List[Int] = {
-    val numa_nodes_linux = Path.explode("/sys/devices/system/node/online")
+  private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")
 
-    val Single = """^(\d+)$""".r
-    val Multiple = """^(\d+)-(\d+)$""".r
+  private val Info_Single = """^(\d+)$""".r
+  private val Info_Multiple = """^(\d+)-(\d+)$""".r
 
-    def read(s: String): List[Int] =
-      s match {
-        case Single(Value.Int(i)) => List(i)
-        case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
-        case _ => error("Cannot parse CPU node specification: " + quote(s))
-      }
+  private def parse_nodes(s: String): List[Int] =
+    s match {
+      case Info_Single(Value.Int(i)) => List(i)
+      case Info_Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
+      case _ => error("Cannot parse CPU node specification: " + quote(s))
+    }
 
-    if (numa_nodes_linux.is_file) {
-      space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read)
-    }
-    else Nil
+  def nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = {
+    val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None
+    for {
+      path <- numa_info.toList
+      if enabled && ssh.is_file(path)
+      s <- space_explode(',', ssh.read(path).trim)
+      n <- parse_nodes(s)
+    } yield n
   }
 
 

--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 11:19:39 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 11:20:42 2023 +0100
@@ -119,7 +119,7 @@
             }
         }
 
-      val numa_nodes = if (numa_shuffling) NUMA.nodes() else Nil
+      val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
       new Context(store, deps, sessions, ordering, progress, numa_nodes,
         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
         no_build = no_build, verbose = verbose, session_setup)