# HG changeset patch
# User wenzelm
# Date 1368817561 -7200
# Node ID 4f91262e7f334c0ad5a43df0f56e63495c516e33
# Parent  1a52aa84e411a19b61a710a102b4f4ac22995825
added isabelle tty option -o;

diff -r 1a52aa84e411 -r 4f91262e7f33 lib/Tools/tty
--- a/lib/Tools/tty	Fri May 17 21:02:08 2013 +0200
+++ b/lib/Tools/tty	Fri May 17 21:06:01 2013 +0200
@@ -14,6 +14,7 @@
   echo "  Options are:"
   echo "    -l NAME      logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
   echo "    -m MODE      add print mode for output"
+  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -p NAME      line editor program name"
   echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
   echo
@@ -33,18 +34,24 @@
 
 # options
 
-ISABELLE_OPTIONS="-I"
+declare -a ISABELLE_OPTIONS=("-I")
+
 LOGIC=""
 LINE_EDITOR="$ISABELLE_LINE_EDITOR"
 
-while getopts "l:m:p:" OPT
+while getopts "l:m:p:o:" OPT
 do
   case "$OPT" in
     l)
       LOGIC="$OPTARG"
       ;;
     m)
-      ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
+      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
+      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
+      ;;
+    o)
+      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
+      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
       ;;
     p)
       LINE_EDITOR="$OPTARG"
@@ -66,7 +73,7 @@
 ## main
 
 if [ -n "$LINE_EDITOR" ]; then
-  exec "$LINE_EDITOR" "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
+  exec "$LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
 else
-  exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
+  exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
 fi
diff -r 1a52aa84e411 -r 4f91262e7f33 src/Doc/System/Interfaces.thy
--- a/src/Doc/System/Interfaces.thy	Fri May 17 21:02:08 2013 +0200
+++ b/src/Doc/System/Interfaces.thy	Fri May 17 21:06:01 2013 +0200
@@ -101,6 +101,7 @@
   Options are:
     -l NAME      logic image name (default ISABELLE_LOGIC)
     -m MODE      add print mode for output
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
 
   Run Isabelle process with plain tty interaction and line editor.
@@ -112,6 +113,9 @@
   as the @{executable_def rlwrap} wrapper for GNU readline); the
   fall-back is to use raw standard input.
 
+  \medskip Option @{verbatim "-o"} allows to override Isabelle system
+  options for this process, see also \secref{sec:system-options}.
+
   Regular interaction works via the standard Isabelle/Isar toplevel
   loop.  The Isar command @{command exit} drops out into the
   bare-bones ML system, which is occasionally useful for debugging of