bin/isabelle
author wenzelm
Mon Jan 05 12:56:22 1998 +0100 (1998-01-05)
changeset 4516 f90b2d459a1b
parent 4355 68c7c544570c
child 4539 4227bd14dbe7
permissions -rwxr-xr-x
added -u option (again);
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # Basic Isabelle startup script.
     6 
     7 
     8 ## settings
     9 
    10 PRG=$(basename $0)
    11 
    12 ISABELLE_HOME=$(dirname $0)/..
    13 . $ISABELLE_HOME/lib/scripts/getsettings || \
    14   { echo "$PRG probably not called from its original place!"; exit 2; }
    15 
    16 
    17 ## diagnostics
    18 
    19 function usage()
    20 {
    21   echo
    22   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
    23   echo
    24   echo "  Options are:"
    25   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    26   echo "    -m MODE      add print mode for output"
    27   echo "    -q           non-interactive session"
    28   echo "    -r           open heap file read-only"
    29   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    30   echo "    -w           reset write permissions on OUTPUT"
    31   echo
    32   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    33   echo "  These are either names to be searched in the Isabelle path, or actual"
    34   echo "  file names (then containing at least one /)."
    35   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    36   echo
    37   exit 1
    38 }
    39 
    40 function fail()
    41 {
    42   echo "$1" >&2
    43   exit 2
    44 }
    45 
    46 
    47 ## process command line
    48 
    49 # options
    50 
    51 MLTEXT=""
    52 MODES=""
    53 TERMINATE=""
    54 READONLY=""
    55 NOWRITE=""
    56 
    57 while getopts "e:m:qruw" OPT
    58 do
    59   case "$OPT" in
    60     e)
    61       MLTEXT="$MLTEXT $OPTARG"
    62       ;;
    63     m)
    64       if [ -z "$MODES" ]; then
    65         MODES="\"$OPTARG\""
    66       else
    67         MODES="\"$OPTARG\", $MODES"
    68       fi
    69       ;;
    70     q)
    71       TERMINATE=true
    72       ;;
    73     r)
    74       READONLY=true
    75       ;;
    76     u)
    77       MLTEXT="$MLTEXT use\"ROOT.ML\";"
    78       ;;
    79     w)
    80       NOWRITE=true
    81       ;;
    82     \?)
    83       usage
    84       ;;
    85   esac
    86 done
    87 
    88 shift $(($OPTIND - 1))
    89 
    90 
    91 # args
    92 
    93 INPUT=""
    94 OUTPUT=""
    95 
    96 if [ $# -ge 1 ]; then
    97   INPUT="$1"
    98   shift
    99 fi
   100 
   101 if [ $# -ge 1 ]; then
   102   OUTPUT="$1"
   103   shift
   104 fi
   105 
   106 [ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
   107 
   108 
   109 ## check ML system
   110 
   111 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   112 
   113 
   114 ## input heap file
   115 
   116 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   117 
   118 case "$INPUT" in
   119   RAW_ML_SYSTEM)
   120     INFILE=""
   121     ;;
   122   */*)
   123     INFILE="$INPUT"
   124     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   125     ;;
   126   *)
   127     ISA_PATH=""
   128     INFILE=""
   129     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   130     do
   131       ISA_PATH="$ISA_PATH $DIR"
   132       [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT
   133     done
   134     if [ -z "$INFILE" ]; then
   135       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   136       for DIR in $ISA_PATH
   137       do
   138         echo "  $DIR" >&2
   139       done
   140       exit 2
   141     fi
   142     ;;
   143 esac
   144 
   145 
   146 ## output heap file
   147 
   148 case "$OUTPUT" in
   149   "")
   150     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   151     ;;
   152   */*)
   153     OUTFILE="$OUTPUT"
   154     ;;
   155   *)
   156     mkdir -p "$ISABELLE_OUTPUT"
   157     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   158     ;;
   159 esac
   160 
   161 
   162 ## prepare tmp directory
   163 
   164 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   165 
   166 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
   167 mkdir -p "$ISABELLE_TMP"
   168 
   169 
   170 ## run it!
   171 
   172 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   173 
   174 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   175 
   176 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   177 
   178 if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
   179   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   180 else
   181   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   182 fi
   183 RC=$?
   184 
   185 #Do not even think of 'rm -r'!!
   186 rmdir $ISABELLE_TMP
   187 
   188 exit $RC