--- 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
--- 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
--- 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
--- 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