# HG changeset patch
# User wenzelm
# Date 1405871641 -7200
# Node ID 74bbe9317aa4dfcdad3b4c9acd248379212a6576
# Parent  86b413b8f779522f62e2099349017f26a3611657
provide explicit options file -- avoid multiple Scala/JVM invocation;

diff -r 86b413b8f779 -r 74bbe9317aa4 bin/isabelle_process
--- 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
diff -r 86b413b8f779 -r 74bbe9317aa4 lib/Tools/console
--- 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
diff -r 86b413b8f779 -r 74bbe9317aa4 src/Doc/System/Basics.thy
--- 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.
diff -r 86b413b8f779 -r 74bbe9317aa4 src/Pure/Tools/build_console.scala
--- 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,