# HG changeset patch
# User wenzelm
# Date 849546808 -3600
# Node ID c1c5652600f1089b3975dbc06c245e2a51ba9329
# Parent  fbd14a05fb888352ec1afadef2e14f69b099805d
isabelle: Basic Isabelle startup script.

diff -r fbd14a05fb88 -r c1c5652600f1 bin/isabelle
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle	Mon Dec 02 18:13:28 1996 +0100
@@ -0,0 +1,162 @@
+#!/bin/bash
+#
+# Basic Isabelle startup script.
+#
+# $Id$
+
+
+## settings
+
+ISABELLE_HOME=$(dirname $(dirname $0))
+. $ISABELLE_HOME/lib/scripts/getsettings
+
+#get bash-style platform info
+unset HOSTTYPE
+unset OSTYPE
+PLATFORM=$(bash -noprofile -c 'echo $HOSTTYPE-$OSTYPE')
+
+
+## diagnostics
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
+  echo
+  echo "  Options are:"
+  echo "    -c           force copying of heap file"
+  echo "    -e MLTEXT    pass MLTEXT to ML session"
+#FIXME  echo "    -o OPTIONS   pass options to ML system"
+  echo "    -q           non-interactive session"
+  echo "    -r           open heap file read-only"
+  echo "    -u           pass 'use\"ROOT.ML\" handle _ => exit 1; commit();'"
+  echo "                 to the ML session"
+  echo
+  echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
+  echo "  These are either names to be searched in the Isabelle path, or actual"
+  echo "  file names (containing at least one /)."
+  echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1"
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+COPYDB=""
+MLTEXT=""
+COPYDB=""
+OPTIONS=""
+TERMINATE=""
+READONLY=""
+
+while getopts "ce:qru" OPT
+do
+  case "$OPT" in
+    c)
+      COPYDB=true
+      ;;
+    e)
+      MLTEXT="$MLTEXT $OPTARG"
+      ;;
+    o)
+      OPTIONS="$OPTIONS $OPTARG"
+      ;;
+    q)
+      TERMINATE=true
+      ;;
+    r)
+      READONLY=true
+      ;;
+    u)
+      MLTEXT="$MLTEXT use\"ROOT.ML\" handle _ => exit 1; commit();"
+      ;;
+    \?)
+      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 ] && fail "Bad args: $*"
+
+
+## check ML system
+
+[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Sorry, no Isabelle."
+
+
+## input heap file
+
+[ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
+
+case "$INPUT" in
+  SYSTEM)
+    INFILE=""
+    ;;
+  */*)
+    INFILE="$INPUT"
+    [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
+    ;;
+  *)
+    INFILE=""
+    for DIR in $(echo $ISABELLE_PATH | tr : " ")
+    do
+      [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
+    done
+    [ -z "$INFILE" ] && fail "Unknown logic: \"$INPUT\""
+    ;;
+esac
+
+
+## output heap file
+
+case "$OUTPUT" in
+  "")
+    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
+    ;;
+  */*)
+    OUTFILE="$OUTPUT"
+    ;;
+  *)
+    OUTDIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
+    mkdir -p "$OUTDIR"
+    OUTFILE="$OUTDIR/$OUTPUT"
+    ;;
+esac
+
+
+## run it!
+
+ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
+
+export INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE
+[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
+exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE