# HG changeset patch
# User wenzelm
# Date 1475404158 -7200
# Node ID ac96fe9224f6d63556c7369f1472dc974b06a5ed
# Parent  c7a4b03727aebd25c8a53dc62e1f6a96814555cd
just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;

diff -r c7a4b03727ae -r ac96fe9224f6 NEWS
--- a/NEWS	Sat Oct 01 23:05:25 2016 +0200
+++ b/NEWS	Sun Oct 02 12:29:18 2016 +0200
@@ -972,11 +972,8 @@
 
 * 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").
+multiprocessor systems. The "isabelle jedit" tool allows to override the
+implicit default via option -p.
 
 
 
diff -r c7a4b03727ae -r ac96fe9224f6 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Oct 01 23:05:25 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sun Oct 02 12:29:18 2016 +0200
@@ -238,6 +238,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)
     -s           system build mode for session image
 
   Start jEdit with Isabelle plugin setup and open FILES
@@ -294,6 +295,10 @@
   name (e.g.\ \<^verbatim>\<open>Isabelle2016\<close>). Thus @{tool jedit_client} can connect to the
   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
+  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
   name, e.g.\ use \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name\<close> and
   \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.
diff -r c7a4b03727ae -r ac96fe9224f6 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 01 23:05:25 2016 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 02 12:29:18 2016 +0200
@@ -98,7 +98,6 @@
   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"
@@ -134,7 +133,6 @@
 
 BUILD_ONLY=false
 BUILD_JARS="jars"
-JAVA_PROCESS_POLICY=""
 ML_PROCESS_POLICY=""
 JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC=""
@@ -144,7 +142,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:J:P:bd:fj:l:m:np:s" OPT
+  while getopts "D:J:bd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
       D)
@@ -153,9 +151,6 @@
       J)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;
-      P)
-        JAVA_PROCESS_POLICY="$OPTARG"
-        ;;
       b)
         BUILD_ONLY=true
         ;;
@@ -373,5 +368,5 @@
   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 $JAVA_PROCESS_POLICY isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
+  exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
 fi