--- a/bin/isabelle_process Sun Jul 20 17:21:14 2014 +0200
+++ b/bin/isabelle_process Sun Jul 20 17:54:01 2014 +0200
@@ -27,6 +27,7 @@
echo
echo " Options are:"
echo " -I startup Isar interaction mode"
+ echo " -O system options from given YXML file"
echo " -P startup Proof General interaction mode"
echo " -S secure mode -- disallow critical operations"
echo " -T ADDR startup process wrapper, with socket address"
@@ -58,6 +59,7 @@
# options
ISAR=""
+OPTIONS_FILE=""
PROOFGENERAL=""
SECURE=""
WRAPPER_SOCKET=""
@@ -69,12 +71,15 @@
READONLY=""
NOWRITE=""
-while getopts "IPST:W:e:m:o:qrw" OPT
+while getopts "IO:PST:W:e:m:o:qrw" OPT
do
case "$OPT" in
I)
ISAR=true
;;
+ O)
+ OPTIONS_FILE="$OPTARG"
+ ;;
P)
PROOFGENERAL=true
;;
@@ -220,8 +225,15 @@
MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
else
ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
- "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
- fail "Failed to retrieve Isabelle system options"
+ if [ -n "$OPTIONS_FILE" ]; then
+ [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \
+ fail "Cannot provide options file and options on command-line"
+ mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" ||
+ fail "Failed to move options file \"$OPTIONS_FILE\""
+ else
+ "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
+ fail "Failed to retrieve Isabelle system options"
+ fi
if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
fi
--- a/lib/Tools/console Sun Jul 20 17:21:14 2014 +0200
+++ b/lib/Tools/console Sun Jul 20 17:54:01 2014 +0200
@@ -35,7 +35,7 @@
declare -a INCLUDE_DIRS=()
LOGIC="$ISABELLE_LOGIC"
NO_BUILD="false"
-declare -a BUILD_OPTIONS=()
+declare -a SYSTEM_OPTIONS=()
SYSTEM_MODE="false"
while getopts "d:l:m:no:s" OPT
@@ -55,9 +55,7 @@
NO_BUILD="true"
;;
o)
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
- BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
+ SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
;;
s)
SYSTEM_MODE="true"
@@ -82,9 +80,17 @@
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
+OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
+
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
- "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" \
- "${INCLUDE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" || exit "$?"
+ "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
+ "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
+ rm -f "$OPTIONS_FILE"
+ exit "$?"
+}
+
+ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
+ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
then
--- a/src/Doc/System/Basics.thy Sun Jul 20 17:21:14 2014 +0200
+++ b/src/Doc/System/Basics.thy Sun Jul 20 17:54:01 2014 +0200
@@ -363,6 +363,7 @@
Options are:
-I startup Isar interaction mode
+ -O system options from given YXML file
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
-T ADDR startup process wrapper, with socket address
@@ -396,7 +397,7 @@
text {*
If the input heap file does not have write permission bits set, or
- the @{verbatim "-r"} option is given explicitely, then the session
+ the @{verbatim "-r"} option is given explicitly, then the session
started will be read-only. That is, the ML world cannot be
committed back into the image file. Otherwise, a writable session
enables commits into either the input file, or into another output
@@ -431,6 +432,9 @@
\medskip Option @{verbatim "-o"} allows to override Isabelle system
options for this process, see also \secref{sec:system-options}.
+ Alternatively, option @{verbatim "-O"} specifies the full environment of
+ system options as a file in YXML format (according to the Isabelle/Scala
+ function @{verbatim isabelle.Options.encode}).
\medskip The @{verbatim "-I"} option makes Isabelle enter Isar
interaction mode on startup, instead of the primitive ML top-level.
--- a/src/Pure/Tools/build_console.scala Sun Jul 20 17:21:14 2014 +0200
+++ b/src/Pure/Tools/build_console.scala Sun Jul 20 17:54:01 2014 +0200
@@ -40,8 +40,11 @@
session ::
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
- Command_Line.Chunks(dirs, build_options) =>
- val options = (Options.init() /: build_options)(_ + _)
+ options_file ::
+ Command_Line.Chunks(dirs, system_options) =>
+ val options = (Options.init() /: system_options)(_ + _)
+ File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
+
val progress = new Build.Console_Progress()
progress.interrupt_handler {
build_console(options, progress,