--- a/bin/isabelle-process Tue Dec 04 21:09:37 2007 +0100
+++ b/bin/isabelle-process Tue Dec 04 22:49:21 2007 +0100
@@ -32,11 +32,11 @@
echo " -P startup Proof General interaction mode"
echo " -S secure mode -- disallow critical operations"
echo " -X startup PGIP interaction mode"
+ echo " -W startup process wrapper (interaction via external program)"
echo " -c tell ML system to compress output image"
echo " -e MLTEXT pass MLTEXT to the ML session"
echo " -f pass 'Session.finish();' to the ML session"
echo " -m MODE add print mode for output"
- echo " -p echo ISABELLE_PID on startup"
echo " -q non-interactive session"
echo " -r open heap file read-only"
echo " -u pass 'use\"ROOT.ML\";' to the ML session"
@@ -65,15 +65,16 @@
ISAR=false
PROOFGENERAL=""
SECURE=""
+WRAPPER=""
+PGIP=""
COMPRESS=""
MLTEXT=""
MODES=""
-ECHOPID=""
TERMINATE=""
READONLY=""
NOWRITE=""
-while getopts "XCIPSce:fm:pqruw" OPT
+while getopts "CIPSWXce:fm:qruw" OPT
do
case "$OPT" in
C)
@@ -88,6 +89,9 @@
S)
SECURE=true
;;
+ W)
+ WRAPPER=true
+ ;;
X)
PGIP=true
;;
@@ -107,9 +111,6 @@
MODES="\"$OPTARG\", $MODES"
fi
;;
- p)
- ECHOPID=true
- ;;
q)
TERMINATE=true
;;
@@ -221,7 +222,9 @@
[ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
-if [ -n "$PGIP" ]; then
+if [ -n "$WRAPPER" ]; then
+ MLTEXT="$MLTEXT; IsabelleProcess.init();"
+elif [ -n "$PGIP" ]; then
MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
elif [ -n "$PROOFGENERAL" ]; then
MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
@@ -232,8 +235,6 @@
export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
ISABELLE_PID ISABELLE_TMP
-[ -n "$ECHOPID" ] && echo "ISABELLE_PID=$ISABELLE_PID"
-
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
"$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else