--- 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)
--- 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"
--- 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,
--- 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
--- 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")))
}