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