# HG changeset patch
# User wenzelm
# Date 1677769762 -3600
# Node ID 291f5848bf551feea8dd7ade437c411425253ed4
# Parent  10147ecf9196593538a2841c1ca77325bd9d72ba
clarified names;

diff -r 10147ecf9196 -r 291f5848bf55 NEWS
--- a/NEWS	Thu Mar 02 15:55:20 2023 +0100
+++ b/NEWS	Thu Mar 02 16:09:22 2023 +0100
@@ -259,6 +259,10 @@
 scalable, and supports most options from "isabelle build". Partial
 builds are supported as well, e.g. "isabelle update -n -a".
 
+* System option "ML_process_policy" has been renamed to
+"process_policy", as it may affect other processes as well (notably in
+"isabelle build").
+
 * Isabelle/Scala provides generic support for XZ and Zstd compression,
 via Compress.Options and Compress.Cache. Bytes.uncompress automatically
 detects the compression scheme.
diff -r 10147ecf9196 -r 291f5848bf55 etc/options
--- a/etc/options	Thu Mar 02 15:55:20 2023 +0100
+++ b/etc/options	Thu Mar 02 16:09:22 2023 +0100
@@ -132,6 +132,9 @@
 option timeout_build : bool = true
   -- "observe timeout for session build"
 
+option process_policy : string = ""
+  -- "command prefix for underlying process, notably ML with NUMA policy"
+
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
@@ -165,9 +168,6 @@
 public option ML_system_apple : bool = true
   -- "prefer native Apple/ARM64 platform (change requires restart)"
 
-public option ML_process_policy : string = ""
-  -- "ML process command prefix (process policy)"
-
 
 section "Build Process"
 
diff -r 10147ecf9196 -r 291f5848bf55 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Thu Mar 02 16:09:22 2023 +0100
@@ -243,7 +243,7 @@
     -l NAME      logic image name
     -m MODE      add print mode for output
     -n           no build of session image on startup
-    -p CMD       ML process command prefix (process policy)
+    -p CMD       command prefix for ML process (e.g. NUMA policy)
     -s           system build mode for session image (system_heaps=true)
     -u           user build mode for session image (system_heaps=false)
 
@@ -308,7 +308,7 @@
   Isabelle desktop application without further options.
 
   The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
-  option @{system_option_ref ML_process_policy} for ML processes started by
+  option @{system_option_ref process_policy} for ML processes started by
   the Prover IDE, e.g. to control CPU affinity on multiprocessor systems.
 
   The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different server
diff -r 10147ecf9196 -r 291f5848bf55 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Pure/ML/ml_process.scala	Thu Mar 02 16:09:22 2023 +0100
@@ -117,7 +117,7 @@
     bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
     bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
 
-    val process_policy = options.string("ML_process_policy")
+    val process_policy = options.string("process_policy")
     val process_prefix = if_proper(process_policy, process_policy + " ")
 
     Bash.process(process_prefix + "\"$POLYML_EXE\" -q " + Bash.strings(bash_args),
diff -r 10147ecf9196 -r 291f5848bf55 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Pure/System/host.scala	Thu Mar 02 16:09:22 2023 +0100
@@ -54,7 +54,7 @@
   def process_policy_options(options: Options, numa_node: Option[Int]): Options =
     numa_node match {
       case None => options
-      case Some(n) => options.string("ML_process_policy") = process_policy(n)
+      case Some(n) => options.string("process_policy") = process_policy(n)
     }
 
   def perhaps_process_policy_options(options: Options): Options = {
diff -r 10147ecf9196 -r 291f5848bf55 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 02 16:09:22 2023 +0100
@@ -203,7 +203,7 @@
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -p CMD       ML process command prefix (process policy)
+    -p CMD       command prefix for ML process (e.g. NUMA policy)
     -s           system build mode for session image (system_heaps=true)
     -u           user build mode for session image (system_heaps=false)
     -v           verbose logging of language server
@@ -226,7 +226,7 @@
           "m:" -> (arg => modes = modes ::: List(arg)),
           "n" -> (_ => no_build = true),
           "o:" -> add_option,
-          "p:" -> (arg => add_option("ML_process_policy=" + arg)),
+          "p:" -> (arg => add_option("process_policy=" + arg)),
           "s" -> (_ => add_option("system_heaps=true")),
           "u" -> (_ => add_option("system_heaps=false")),
           "v" -> (_ => verbose = true))
diff -r 10147ecf9196 -r 291f5848bf55 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Mar 02 16:09:22 2023 +0100
@@ -28,7 +28,7 @@
   echo "    -l NAME      logic session name"
   echo "    -m MODE      add print mode for output"
   echo "    -n           no build of session image on startup"
-  echo "    -p CMD       ML process command prefix (process policy)"
+  echo "    -p CMD       command prefix for ML process (e.g. NUMA policy)"
   echo "    -s           system build mode for session image (system_heaps=true)"
   echo "    -u           user build mode for session image (system_heaps=false)"
   echo
@@ -56,7 +56,7 @@
 
 BUILD_ONLY=false
 BUILD_OPTIONS=""
-ML_PROCESS_POLICY=""
+PROCESS_POLICY=""
 JEDIT_LOGIC_ANCESTOR=""
 JEDIT_LOGIC_REQUIREMENTS=""
 JEDIT_INCLUDE_SESSIONS=""
@@ -119,7 +119,7 @@
         JEDIT_NO_BUILD="true"
         ;;
       p)
-        ML_PROCESS_POLICY="$OPTARG"
+        PROCESS_POLICY="$OPTARG"
         ;;
       s)
         JEDIT_BUILD_MODE="system"
@@ -163,7 +163,7 @@
 
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
     JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
-  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
+  export JEDIT_PROCESS_POLICY="$PROCESS_POLICY"
   exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
     "${JAVA_ARGS[@]}" isabelle.jedit.JEdit_Main "${ARGS[@]}"
 fi
diff -r 10147ecf9196 -r 291f5848bf55 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Mar 02 16:09:22 2023 +0100
@@ -28,9 +28,9 @@
       }
 
     val options2 =
-      Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
+      Isabelle_System.getenv("JEDIT_PROCESS_POLICY") match {
         case "" => options1
-        case s => options1.string.update("ML_process_policy", s)
+        case s => options1.string.update("process_policy", s)
       }
 
     options2