bin/isabelle
author wenzelm
Mon Jul 07 09:05:16 1997 +0200 (1997-07-07)
changeset 3502 ec22ba0a26ec
parent 3203 af42c8cc8e75
child 4333 1d326b826851
permissions -rwxr-xr-x
added -w option;
     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 "    -w           reset write permissions on OUTPUT"
    30   echo
    31   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    32   echo "  These are either names to be searched in the Isabelle path, or actual"
    33   echo "  file names (then containing at least one /)."
    34   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    35   echo
    36   exit 1
    37 }
    38 
    39 function fail()
    40 {
    41   echo "$1" >&2
    42   exit 2
    43 }
    44 
    45 
    46 ## process command line
    47 
    48 # options
    49 
    50 MLTEXT=""
    51 MODES=""
    52 TERMINATE=""
    53 READONLY=""
    54 NOWRITE=""
    55 
    56 while getopts "e:m:qrw" OPT
    57 do
    58   case "$OPT" in
    59     e)
    60       MLTEXT="$MLTEXT $OPTARG"
    61       ;;
    62     m)
    63       if [ -z "$MODES" ]; then
    64         MODES="\"$OPTARG\""
    65       else
    66         MODES="\"$OPTARG\", $MODES"
    67       fi
    68       ;;
    69     q)
    70       TERMINATE=true
    71       ;;
    72     r)
    73       READONLY=true
    74       ;;
    75     w)
    76       NOWRITE=true
    77       ;;
    78     \?)
    79       usage
    80       ;;
    81   esac
    82 done
    83 
    84 shift $(($OPTIND - 1))
    85 
    86 
    87 # args
    88 
    89 INPUT=""
    90 OUTPUT=""
    91 
    92 if [ $# -ge 1 ]; then
    93   INPUT="$1"
    94   shift
    95 fi
    96 
    97 if [ $# -ge 1 ]; then
    98   OUTPUT="$1"
    99   shift
   100 fi
   101 
   102 [ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
   103 
   104 
   105 ## check ML system
   106 
   107 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   108 
   109 
   110 ## input heap file
   111 
   112 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   113 
   114 case "$INPUT" in
   115   RAW_ML_SYSTEM)
   116     INFILE=""
   117     ;;
   118   */*)
   119     INFILE="$INPUT"
   120     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   121     ;;
   122   *)
   123     ISA_PATH=""
   124     INFILE=""
   125     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   126     do
   127       ISA_PATH="$ISA_PATH $DIR"
   128       [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT
   129     done
   130     if [ -z "$INFILE" ]; then
   131       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   132       for DIR in $ISA_PATH
   133       do
   134         echo "  $DIR" >&2
   135       done
   136       exit 2
   137     fi
   138     ;;
   139 esac
   140 
   141 
   142 ## output heap file
   143 
   144 case "$OUTPUT" in
   145   "")
   146     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   147     ;;
   148   */*)
   149     OUTFILE="$OUTPUT"
   150     ;;
   151   *)
   152     mkdir -p "$ISABELLE_OUTPUT"
   153     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   154     ;;
   155 esac
   156 
   157 
   158 ## run it!
   159 
   160 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   161 
   162 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   163 
   164 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE
   165 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   166 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE