bin/isabelle
changeset 2704 afa01c9f1ab0
parent 2591 ae16f162f973
child 2711 098f9ce0541a
     1.1 --- a/bin/isabelle	Fri Feb 28 16:55:35 1997 +0100
     1.2 +++ b/bin/isabelle	Fri Feb 28 16:56:31 1997 +0100
     1.3 @@ -7,14 +7,27 @@
     1.4  
     1.5  ## settings
     1.6  
     1.7 +PRG=$(basename $0)
     1.8 +
     1.9  ISABELLE_HOME=$(dirname $(dirname $0))
    1.10 -. $ISABELLE_HOME/lib/scripts/getsettings || exit 2
    1.11 +case "$ISABELLE_HOME" in
    1.12 +  /*)
    1.13 +    if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
    1.14 +      . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
    1.15 +    else
    1.16 +      echo "ERROR: $PRG probably not called from its original place!"
    1.17 +      exit 1
    1.18 +    fi
    1.19 +    ;;
    1.20 +  *)
    1.21 +    echo "ERROR: $PRG not called with absolute path specification!"
    1.22 +    exit 1
    1.23 +    ;;
    1.24 +esac
    1.25  
    1.26  
    1.27  ## diagnostics
    1.28  
    1.29 -PRG=$(basename $0)
    1.30 -
    1.31  function usage()
    1.32  {
    1.33    echo
    1.34 @@ -23,6 +36,7 @@
    1.35    echo "  Options are:"
    1.36    echo "    -c           force copying of heap file (for Poly/ML)"
    1.37    echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.38 +  echo "    -m MODE      add print mode for output"
    1.39    echo "    -q           non-interactive session"
    1.40    echo "    -r           open heap file read-only"
    1.41    echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
    1.42 @@ -49,10 +63,11 @@
    1.43  COPYDB=""
    1.44  MLTEXT=""
    1.45  COPYDB=""
    1.46 +MODES=""
    1.47  TERMINATE=""
    1.48  READONLY=""
    1.49  
    1.50 -while getopts "ce:qru" OPT
    1.51 +while getopts "ce:m:qru" OPT
    1.52  do
    1.53    case "$OPT" in
    1.54      c)
    1.55 @@ -61,6 +76,13 @@
    1.56      e)
    1.57        MLTEXT="$MLTEXT $OPTARG"
    1.58        ;;
    1.59 +    m)
    1.60 +      if [ -z "$MODES" ]; then
    1.61 +        MODES="\"$OPTARG\""
    1.62 +      else
    1.63 +        MODES="$MODES, \"$OPTARG\""
    1.64 +      fi
    1.65 +      ;;
    1.66      q)
    1.67        TERMINATE=true
    1.68        ;;
    1.69 @@ -155,6 +177,8 @@
    1.70  
    1.71  ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    1.72  
    1.73 +[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.74 +
    1.75  export INFILE OUTFILE COPYDB MLTEXT TERMINATE
    1.76  [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
    1.77  exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE