# HG changeset patch
# User wenzelm
# Date 999972031 -7200
# Node ID 915c5de6480f1b0b801c3f167dfc7e679691979a
# Parent  e7265e70fd7c906baf8e4a32bc643b1f69252937
smart selection of isabelle-process versus isabelle-interface;

diff -r e7265e70fd7c -r 915c5de6480f bin/isabelle
--- 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" "$@"
diff -r e7265e70fd7c -r 915c5de6480f bin/isabelle-interface
--- /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" "$@"
diff -r e7265e70fd7c -r 915c5de6480f bin/isabelle-process
--- /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"
diff -r e7265e70fd7c -r 915c5de6480f lib/Tools/install
--- 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"