bin/isabelle
changeset 2343 2588b63b42ca
parent 2308 641be5ad47af
child 2395 c24a79fe3651
     1.1 --- a/bin/isabelle	Mon Dec 09 16:33:57 1996 +0100
     1.2 +++ b/bin/isabelle	Mon Dec 09 16:38:07 1996 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -#!/bin/bash
     1.5 +#!/bin/bash -norc
     1.6  #
     1.7  # $Id$
     1.8  #
     1.9 @@ -9,11 +9,7 @@
    1.10  
    1.11  ISABELLE_HOME=$(dirname $(dirname $0))
    1.12  . $ISABELLE_HOME/lib/scripts/getsettings
    1.13 -
    1.14 -#get bash-style platform info
    1.15 -unset HOSTTYPE
    1.16 -unset OSTYPE
    1.17 -PLATFORM=$(bash -noprofile -c 'echo $HOSTTYPE-$OSTYPE')
    1.18 +. $ISABELLE_HOME/lib/scripts/getplatform
    1.19  
    1.20  
    1.21  ## diagnostics
    1.22 @@ -27,16 +23,14 @@
    1.23    echo
    1.24    echo "  Options are:"
    1.25    echo "    -c           force copying of heap file"
    1.26 -  echo "    -e MLTEXT    pass MLTEXT to ML session"
    1.27 -#FIXME  echo "    -o OPTIONS   pass options to ML system"
    1.28 +  echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.29    echo "    -q           non-interactive session"
    1.30    echo "    -r           open heap file read-only"
    1.31 -  echo "    -u           pass 'use\"ROOT.ML\" handle _ => exit 1; commit();'"
    1.32 -  echo "                 to the ML session"
    1.33 +  echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
    1.34    echo
    1.35    echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    1.36    echo "  These are either names to be searched in the Isabelle path, or actual"
    1.37 -  echo "  file names (containing at least one /)."
    1.38 +  echo "  file names (then containing at least one /)."
    1.39    echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
    1.40    echo
    1.41    exit 1
    1.42 @@ -44,7 +38,7 @@
    1.43  
    1.44  function fail()
    1.45  {
    1.46 -  echo "$1"
    1.47 +  echo "$1" >&2
    1.48    exit 2
    1.49  }
    1.50  
    1.51 @@ -56,7 +50,6 @@
    1.52  COPYDB=""
    1.53  MLTEXT=""
    1.54  COPYDB=""
    1.55 -OPTIONS=""
    1.56  TERMINATE=""
    1.57  READONLY=""
    1.58  
    1.59 @@ -69,9 +62,6 @@
    1.60      e)
    1.61        MLTEXT="$MLTEXT $OPTARG"
    1.62        ;;
    1.63 -    o)
    1.64 -      OPTIONS="$OPTIONS $OPTARG"
    1.65 -      ;;
    1.66      q)
    1.67        TERMINATE=true
    1.68        ;;
    1.69 @@ -79,7 +69,7 @@
    1.70        READONLY=true
    1.71        ;;
    1.72      u)
    1.73 -      MLTEXT="$MLTEXT use\"ROOT.ML\" handle _ => exit 1; commit();"
    1.74 +      MLTEXT="$MLTEXT exit_use_dir\".\";"
    1.75        ;;
    1.76      \?)
    1.77        usage
    1.78 @@ -105,7 +95,7 @@
    1.79    shift
    1.80  fi
    1.81  
    1.82 -[ $# -ne 0 ] && fail "Bad args: $*"
    1.83 +[ $# -ne 0 ] && { echo "Bad args: $*"; usage }
    1.84  
    1.85  
    1.86  ## check ML system
    1.87 @@ -123,7 +113,7 @@
    1.88      ;;
    1.89    */*)
    1.90      INFILE="$INPUT"
    1.91 -    [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
    1.92 +    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
    1.93      ;;
    1.94    *)
    1.95      ISA_PATH=""
    1.96 @@ -134,10 +124,10 @@
    1.97        [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
    1.98      done
    1.99      if [ -z "$INFILE" ]; then
   1.100 -      echo "Unknown logic \"$INPUT\" -- no heap file found in:"
   1.101 +      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   1.102        for DIR in $ISA_PATH
   1.103        do
   1.104 -        echo "  $DIR"
   1.105 +        echo "  $DIR" >&2
   1.106        done
   1.107        exit 2
   1.108      fi
   1.109 @@ -166,6 +156,6 @@
   1.110  
   1.111  ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   1.112  
   1.113 -export INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE
   1.114 +export INFILE OUTFILE COPYDB MLTEXT TERMINATE
   1.115  [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   1.116  exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE