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