# HG changeset patch
# User wenzelm
# Date 1475355925 -7200
# Node ID c7a4b03727aebd25c8a53dc62e1f6a96814555cd
# Parent  4effb93c2a098728052e2ee9284a3cec637e1e8d
options for process policy, notably for multiprocessor machines;

diff -r 4effb93c2a09 -r c7a4b03727ae NEWS
--- a/NEWS	Sat Oct 01 20:59:09 2016 +0200
+++ b/NEWS	Sat Oct 01 23:05:25 2016 +0200
@@ -970,6 +970,14 @@
 exhaust the small 32-bit address space of the ML process (which is used
 by default).
 
+* System option "ML_process_policy" specifies an optional command prefix
+for the underlying ML process, e.g. to control CPU affinity on
+multiprocessor systems.
+
+* The "isabelle jedit" tool provides options -P and -p to specify an
+optional command prefix for the Java and ML process, respectively (see
+also option "ML_process_policy").
+
 
 
 New in Isabelle2016 (February 2016)
diff -r 4effb93c2a09 -r c7a4b03727ae etc/options
--- a/etc/options	Sat Oct 01 20:59:09 2016 +0200
+++ b/etc/options	Sat Oct 01 23:05:25 2016 +0200
@@ -129,6 +129,9 @@
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
+public option ML_process_policy : string = ""
+  -- "ML process command prefix (process policy)"
+
 
 section "Editor Reactivity"
 
diff -r 4effb93c2a09 -r c7a4b03727ae src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Oct 01 20:59:09 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Sat Oct 01 23:05:25 2016 +0200
@@ -98,7 +98,9 @@
       (eval_init ::: eval_modes ::: eval_options ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
-    Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
+    Bash.process(
+      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
+        File.bash_args(bash_args),
       cwd = cwd,
       env =
         Isabelle_System.library_path(env ++ env_options ++ env_tmp,
diff -r 4effb93c2a09 -r c7a4b03727ae src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 01 20:59:09 2016 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 01 23:05:25 2016 +0200
@@ -98,6 +98,7 @@
   echo "  Options are:"
   echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
+  echo "    -P CMD       JVM process command prefix (process policy)"
   echo "    -b           build only"
   echo "    -d DIR       include session directory"
   echo "    -f           fresh build"
@@ -106,6 +107,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 "    -s           system build mode for session image"
   echo
   echo "  Start jEdit with Isabelle plugin setup and open FILES"
@@ -132,6 +134,8 @@
 
 BUILD_ONLY=false
 BUILD_JARS="jars"
+JAVA_PROCESS_POLICY=""
+ML_PROCESS_POLICY=""
 JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
@@ -140,7 +144,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:J:bd:fj:l:m:ns" OPT
+  while getopts "D:J:P:bd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
       D)
@@ -149,6 +153,9 @@
       J)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;
+      P)
+        JAVA_PROCESS_POLICY="$OPTARG"
+        ;;
       b)
         BUILD_ONLY=true
         ;;
@@ -178,6 +185,9 @@
       n)
         JEDIT_BUILD_MODE="none"
         ;;
+      p)
+        ML_PROCESS_POLICY="$OPTARG"
+        ;;
       s)
         JEDIT_BUILD_MODE="system"
         ;;
@@ -361,6 +371,7 @@
 if [ "$BUILD_ONLY" = false ]
 then
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   classpath "$JEDIT_HOME/dist/jedit.jar"
-  exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
+  exec $JAVA_PROCESS_POLICY isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
 fi
diff -r 4effb93c2a09 -r c7a4b03727ae src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Sat Oct 01 20:59:09 2016 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sat Oct 01 23:05:25 2016 +0200
@@ -26,13 +26,19 @@
 
   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
 
+  def session_options(): Options =
+    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
+      case "" => PIDE.options.value
+      case s => PIDE.options.value.string("ML_process_policy") = s
+    }
+
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
 
   def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
   {
     val mode = session_build_mode()
 
-    Build.build(options = PIDE.options.value, progress = progress,
+    Build.build(options = session_options(), progress = progress,
       build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
       dirs = session_dirs(), sessions = List(session_name())).rc
   }
@@ -42,8 +48,9 @@
     val modes =
       (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
        space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
+
     PIDE.session.start(receiver =>
-      Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
+      Isabelle_Process(options = session_options(), logic = session_name(), dirs = session_dirs(),
         modes = modes, receiver = receiver,
         store = Sessions.store(session_build_mode() == "system")))
   }