--- a/bin/isabelle Fri Sep 15 15:48:41 2000 +0200
+++ b/bin/isabelle Fri Sep 15 16:28:04 2000 +0200
@@ -25,6 +25,7 @@
echo
echo " Options are:"
echo " -I startup Isar interaction mode"
+ echo " -P startup ProofGeneral interaction mode"
echo " -c tell ML system to compress output image"
echo " -e MLTEXT pass MLTEXT to the ML session"
echo " -m MODE add print mode for output"
@@ -52,6 +53,8 @@
# options
+ISAR=false
+PROOFGENERAL=""
COMPRESS=""
MLTEXT=""
MODES=""
@@ -59,11 +62,14 @@
READONLY=""
NOWRITE=""
-while getopts "Ice:m:qruw" OPT
+while getopts "IPce:m:qruw" OPT
do
case "$OPT" in
I)
- MLTEXT="$MLTEXT Isar.main();"
+ ISAR=true
+ ;;
+ P)
+ PROOFGENERAL=true
;;
c)
COMPRESS=true
@@ -187,6 +193,12 @@
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
+if [ -n "$PROOFGENERAL" ]; then
+ MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
+elif [ "$ISAR" = true ]; then
+ MLTEXT="$MLTEXT; Isar.main();"
+fi
+
export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then