aboutsummaryrefslogtreecommitdiff
path: root/isar/interface
diff options
context:
space:
mode:
Diffstat (limited to 'isar/interface')
-rw-r--r--isar/interface96
1 files changed, 55 insertions, 41 deletions
diff --git a/isar/interface b/isar/interface
index 71a922f5..8c985092 100644
--- a/isar/interface
+++ b/isar/interface
@@ -27,6 +27,7 @@ usage()
echo
echo " Options are:"
echo " -I BOOL use Isabelle/Isar instead of classic Isabelle (default $ISAR)"
+ echo " -P BOOL actually start Proof General (default true), otherwise plain tty session"
echo " -X BOOL configure the X-Symbol package on startup (default true)"
echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
echo " -m MODE add print mode for output"
@@ -55,6 +56,7 @@ fail()
# options
ISABELLE_OPTIONS=""
+START_PG="true"
LOGIC="$ISABELLE_LOGIC"
PROGNAME="xemacs"
INITFILE="true"
@@ -65,12 +67,15 @@ XSYMBOLSETUP=true
getoptions()
{
OPTIND=1
- while getopts "I:X:l:m:p:u:w:x:" OPT
+ while getopts "I:P:X:l:m:p:u:w:x:" OPT
do
case "$OPT" in
I)
ISAR="$OPTARG"
;;
+ P)
+ START_PG="$OPTARG"
+ ;;
X)
XSYMBOLSETUP="$OPTARG"
;;
@@ -132,49 +137,58 @@ fi
## main
-ARGS=""
+if [ "$START_PG" = false ]; then
-[ "$INITFILE" = false ] && ARGS="$ARGS -q"
+ [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
+ exec "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC"
-if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
- ARGS="$ARGS -T Isabelle"
- [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && "$ISATOOL" installfonts -x
else
- ARGS="$ARGS -nw"
- XSYMBOL=false
-fi
-
-[ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME=""
-
-ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'"
+ ARGS=""
+
+ [ "$INITFILE" = false ] && ARGS="$ARGS -q"
+
+ if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
+ ARGS="$ARGS -T Isabelle"
+ [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && "$ISATOOL" installfonts -x
+ else
+ ARGS="$ARGS -nw"
+ XSYMBOL=false
+ fi
+
+ [ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME=""
+
+
+ ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'"
+
+ if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
+ ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords.el'"
+ elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
+ ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords.el'"
+ fi
+
+ for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
+ "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
+ do
+ [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'"
+ done
+
+ case "$LOGIC" in
+ /*)
+ ;;
+ */*)
+ LOGIC="$PWD/$LOGIC"
+ ;;
+ esac
+
+ PROOFGENERAL_HOME="$SUPER"
+ PROOFGENERAL_ASSISTANTS="$KIND"
+ PROOFGENERAL_LOGIC="$LOGIC"
+ PROOFGENERAL_XSYMBOL="$XSYMBOL"
+
+ export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL
+ export ISABELLE_OPTIONS
+
+ eval exec "$PROGNAME" "$ARGS" "$FILES"
-if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
- ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords.el'"
-elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
- ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords.el'"
fi
-
-for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
- "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
-do
- [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'"
-done
-
-case "$LOGIC" in
- /*)
- ;;
- */*)
- LOGIC="$PWD/$LOGIC"
- ;;
-esac
-
-PROOFGENERAL_HOME="$SUPER"
-PROOFGENERAL_ASSISTANTS="$KIND"
-PROOFGENERAL_LOGIC="$LOGIC"
-PROOFGENERAL_XSYMBOL="$XSYMBOL"
-
-export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL
-export ISABELLE_OPTIONS
-
-eval exec "$PROGNAME" "$ARGS" "$FILES"