# HG changeset patch
# User wenzelm
# Date 1368810292 -7200
# Node ID fc458f304f93211220cb806f4e226cc3d68dde5b
# Parent  10bc73197a570fa16e1e1dc189390600117ca93e
added isabelle-process option -o;

diff -r 10bc73197a57 -r fc458f304f93 bin/isabelle-process
--- a/bin/isabelle-process	Fri May 17 18:50:55 2013 +0200
+++ b/bin/isabelle-process	Fri May 17 19:04:52 2013 +0200
@@ -33,6 +33,7 @@
   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -m MODE      add print mode for output"
+  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -q           non-interactive session"
   echo "    -r           open heap file read-only"
   echo "    -w           reset write permissions on OUTPUT"
@@ -63,11 +64,12 @@
 WRAPPER_FIFOS=""
 MLTEXT=""
 MODES=""
+declare -a SYSTEM_OPTIONS=()
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "IPST:W:e:m:qrw" OPT
+while getopts "IPST:W:e:m:o:qrw" OPT
 do
   case "$OPT" in
     I)
@@ -95,6 +97,9 @@
         MODES="\"$OPTARG\", $MODES"
       fi
       ;;
+    o)
+      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
+      ;;
     q)
       TERMINATE=true
       ;;
@@ -215,7 +220,8 @@
   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
 else
   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
-  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
+  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
+    fail "Failed to retrieve Isabelle system options"
   if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
     MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
   fi
diff -r 10bc73197a57 -r fc458f304f93 lib/Tools/build
--- a/lib/Tools/build	Fri May 17 18:50:55 2013 +0200
+++ b/lib/Tools/build	Fri May 17 19:04:52 2013 +0200
@@ -36,7 +36,7 @@
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -l           list session source files"
   echo "    -n           no build -- test dependencies only"
-  echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
+  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo "    -v           verbose"
   echo
diff -r 10bc73197a57 -r fc458f304f93 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Fri May 17 18:50:55 2013 +0200
+++ b/src/Doc/System/Basics.thy	Fri May 17 19:04:52 2013 +0200
@@ -379,6 +379,7 @@
     -W IN:OUT    startup process wrapper, with input/output fifos
     -e MLTEXT    pass MLTEXT to the ML session
     -m MODE      add print mode for output
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -q           non-interactive session
     -r           open heap file read-only
     -w           reset write permissions on OUTPUT
@@ -438,6 +439,9 @@
   option inhibits interaction, thus providing a pure batch mode
   facility.
 
+  \medskip Option @{verbatim "-s"} allows to override Isabelle system
+  options for this process, see also \secref{sec:system-options}.
+
   \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
   interaction mode on startup, instead of the primitive ML top-level.
   The @{verbatim "-P"} option configures the top-level loop for
diff -r 10bc73197a57 -r fc458f304f93 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Fri May 17 18:50:55 2013 +0200
+++ b/src/Doc/System/Sessions.thy	Fri May 17 19:04:52 2013 +0200
@@ -275,8 +275,7 @@
     -j INT       maximum number of parallel jobs (default 1)
     -l           list session source files
     -n           no build -- test dependencies only
-    -o OPTION    override session configuration OPTION
-                 (via NAME=VAL or NAME)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -s           system build mode: produce output in ISABELLE_HOME
     -v           verbose