--- a/bin/isabelle Tue Sep 04 21:10:57 2001 +0200
+++ b/bin/isabelle Sat Sep 08 20:00:31 2001 +0200
@@ -4,220 +4,12 @@
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
-# Basic Isabelle startup script.
-
-
-## settings
-
-PRG="$(basename "$0")"
-
-ISABELLE_HOME="$(dirname "$0")/.."
-. "$ISABELLE_HOME/lib/scripts/getsettings" || \
- { echo "$PRG probably not called from its original place!"; exit 2; }
-
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
- echo
- echo " Options are:"
- echo " -C tell ML system to copy output image"
- echo " -I startup Isar interaction mode"
- echo " -P startup Proof General interaction mode"
- 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 " -q non-interactive session"
- echo " -r open heap file read-only"
- echo " -u pass 'use\"ROOT.ML\";' to the ML session"
- echo " -w reset write permissions on OUTPUT"
- echo
- echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
- echo " These are either names to be searched in the Isabelle path, or"
- echo " actual file names (containing at least one /)."
- echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
+# Smart selection of isabelle-process versus isabelle-interface.
-COPYDB=""
-ISAR=false
-PROOFGENERAL=""
-COMPRESS=""
-MLTEXT=""
-MODES=""
-TERMINATE=""
-READONLY=""
-NOWRITE=""
-
-while getopts "CIPce:fm:qruw" OPT
-do
- case "$OPT" in
- C)
- COPYDB=true
- ;;
- I)
- ISAR=true
- ;;
- P)
- PROOFGENERAL=true
- ;;
- c)
- COMPRESS=true
- ;;
- e)
- MLTEXT="$MLTEXT $OPTARG"
- ;;
- f)
- MLTEXT="$MLTEXT Session.finish();"
- ;;
- m)
- if [ -z "$MODES" ]; then
- MODES="\"$OPTARG\""
- else
- MODES="\"$OPTARG\", $MODES"
- fi
- ;;
- q)
- TERMINATE=true
- ;;
- r)
- READONLY=true
- ;;
- u)
- MLTEXT="$MLTEXT use\"ROOT.ML\";"
- ;;
- w)
- NOWRITE=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
+THIS=$(cd "$(dirname "$0")"; pwd)
+NAME="$(basename "$0")"
-
-# args
-
-INPUT=""
-OUTPUT=""
-
-if [ "$#" -ge 1 ]; then
- INPUT="$1"
- shift
-fi
-
-if [ "$#" -ge 1 ]; then
- OUTPUT="$1"
- shift
-fi
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## check ML system
-
-[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
-
-
-## input heap file
-
-[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
-
-case "$INPUT" in
- RAW_ML_SYSTEM)
- INFILE=""
- ;;
- */*)
- INFILE="$INPUT"
- [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
- ;;
- *)
- INFILE=""
- ISA_PATH=""
-
- ORIG_IFS="$IFS"
- IFS=":"
- for DIR in $ISABELLE_PATH
- do
- DIR="$DIR/$ML_IDENTIFIER"
- ISA_PATH="$ISA_PATH $DIR\n"
- [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
- done
- IFS="$ORIG_IFS"
+PRG=isabelle-interface
+[ "$NAME" = isabelle ] && PRG=isabelle-process
- if [ -z "$INFILE" ]; then
- echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
- echo -ne "$ISA_PATH" >&2
- exit 2
- fi
- ;;
-esac
-
-
-## output heap file
-
-case "$OUTPUT" in
- "")
- [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
- ;;
- */*)
- OUTFILE="$OUTPUT"
- ;;
- *)
- mkdir -p "$ISABELLE_OUTPUT"
- OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
- ;;
-esac
-
-
-## prepare tmp directory
-
-[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-
-ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
-mkdir -p "$ISABELLE_TMP"
-
-
-## run it!
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-
-[ -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 COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
-
-if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
- "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
-else
- "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
-fi
-RC="$?"
-
-#Do not even think of 'rm -r'!!
-rmdir "$ISABELLE_TMP"
-
-exit "$RC"
+exec "$THIS/$PRG" "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle-interface Sat Sep 08 20:00:31 2001 +0200
@@ -0,0 +1,44 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# Isabelle interface startup script.
+
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(dirname "$0")/.."
+. "$ISABELLE_HOME/lib/scripts/getsettings" || \
+ { echo "$PRG probably not called from its original place!"; exit 2; }
+
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## main
+
+case "$ISABELLE_INTERFACE" in
+ none)
+ INTERFACE="$ISABELLE"
+ ;;
+ */*)
+ INTERFACE="$ISABELLE_INTERFACE"
+ ;;
+ *)
+ INTERFACE="$ISABELLE_HOME/lib/scripts/isa-$ISABELLE_INTERFACE"
+ ;;
+esac
+
+[ ! -x "$INTERFACE" ] && fail "Bad Isabelle interface: \"$ISABELLE_INTERFACE\""
+
+exec "$INTERFACE" "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle-process Sat Sep 08 20:00:31 2001 +0200
@@ -0,0 +1,222 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# Isabelle process startup script.
+
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(dirname "$0")/.."
+. "$ISABELLE_HOME/lib/scripts/getsettings" || \
+ { echo "$PRG probably not called from its original place!"; exit 2; }
+
+
+## diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
+ echo
+ echo " Options are:"
+ echo " -C tell ML system to copy output image"
+ echo " -I startup Isar interaction mode"
+ echo " -P startup Proof General interaction mode"
+ 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 " -q non-interactive session"
+ echo " -r open heap file read-only"
+ echo " -u pass 'use\"ROOT.ML\";' to the ML session"
+ echo " -w reset write permissions on OUTPUT"
+ echo
+ echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
+ echo " These are either names to be searched in the Isabelle path, or"
+ echo " actual file names (containing at least one /)."
+ echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+COPYDB=""
+ISAR=false
+PROOFGENERAL=""
+COMPRESS=""
+MLTEXT=""
+MODES=""
+TERMINATE=""
+READONLY=""
+NOWRITE=""
+
+while getopts "CIPce:fm:qruw" OPT
+do
+ case "$OPT" in
+ C)
+ COPYDB=true
+ ;;
+ I)
+ ISAR=true
+ ;;
+ P)
+ PROOFGENERAL=true
+ ;;
+ c)
+ COMPRESS=true
+ ;;
+ e)
+ MLTEXT="$MLTEXT $OPTARG"
+ ;;
+ f)
+ MLTEXT="$MLTEXT Session.finish();"
+ ;;
+ m)
+ if [ -z "$MODES" ]; then
+ MODES="\"$OPTARG\""
+ else
+ MODES="\"$OPTARG\", $MODES"
+ fi
+ ;;
+ q)
+ TERMINATE=true
+ ;;
+ r)
+ READONLY=true
+ ;;
+ u)
+ MLTEXT="$MLTEXT use\"ROOT.ML\";"
+ ;;
+ w)
+ NOWRITE=true
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+INPUT=""
+OUTPUT=""
+
+if [ "$#" -ge 1 ]; then
+ INPUT="$1"
+ shift
+fi
+
+if [ "$#" -ge 1 ]; then
+ OUTPUT="$1"
+ shift
+fi
+
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+## check ML system
+
+[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
+
+
+## input heap file
+
+[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
+
+case "$INPUT" in
+ RAW_ML_SYSTEM)
+ INFILE=""
+ ;;
+ */*)
+ INFILE="$INPUT"
+ [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
+ ;;
+ *)
+ INFILE=""
+ ISA_PATH=""
+
+ ORIG_IFS="$IFS"
+ IFS=":"
+ for DIR in $ISABELLE_PATH
+ do
+ DIR="$DIR/$ML_IDENTIFIER"
+ ISA_PATH="$ISA_PATH $DIR\n"
+ [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
+ done
+ IFS="$ORIG_IFS"
+
+ if [ -z "$INFILE" ]; then
+ echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
+ echo -ne "$ISA_PATH" >&2
+ exit 2
+ fi
+ ;;
+esac
+
+
+## output heap file
+
+case "$OUTPUT" in
+ "")
+ [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
+ ;;
+ */*)
+ OUTFILE="$OUTPUT"
+ ;;
+ *)
+ mkdir -p "$ISABELLE_OUTPUT"
+ OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
+ ;;
+esac
+
+
+## prepare tmp directory
+
+[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
+mkdir -p "$ISABELLE_TMP"
+
+
+## run it!
+
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+
+[ -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 COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
+
+if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+else
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+fi
+RC="$?"
+
+rmdir "$ISABELLE_TMP"
+
+exit "$RC"
--- a/lib/Tools/install Tue Sep 04 21:10:57 2001 +0200
+++ b/lib/Tools/install Sat Sep 08 20:00:31 2001 +0200
@@ -95,7 +95,7 @@
if [ -n "$BINDIR" ]; then
mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
- for NAME in isatool isabelle Isabelle
+ for NAME in isatool isabelle-process isabelle-interface
do
BIN="$BINDIR/$NAME"
DIST="$DISTDIR/bin/$NAME"
@@ -105,6 +105,14 @@
echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
chmod +x "$BIN"
done
+ for NAME in Isabelle isabelle
+ do
+ BIN="$BINDIR/$NAME"
+ DIST="$DISTDIR/bin/$NAME"
+ echo "installing $BIN"
+ cp "$DIST" "$BIN" || fail "Cannot write file: $BIN"
+ chmod +x "$BIN"
+ done
fi
@@ -138,7 +146,7 @@
echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP"
echo "[KDE Desktop Entry]" >> "$KDEAPP"
echo "Type=Application" >> "$KDEAPP"
- echo "Exec=\"$DISTDIR/bin/Isabelle\" %f" >> "$KDEAPP"
+ echo "Exec=\"$DISTDIR/bin/isabelle-interface\" %f" >> "$KDEAPP"
echo "Icon=isabelle.xpm" >> "$KDEAPP"
echo "TerminalOptions=" >> "$KDEAPP"
echo "Path=" >> "$KDEAPP"