bin/isabelle
author wenzelm
Fri Apr 11 17:30:15 1997 +0200 (1997-04-11)
changeset 2936 bd33e7aae062
parent 2768 bc6d915b8019
child 2968 8ba30b031f31
permissions -rwxr-xr-x
fixed { ... } shell syntax to accomodate bash 2.x;
     1 #!/bin/bash -norc
     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 "    -c           force copying of heap file (for Poly/ML)"
    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 'exit_use_dir\".\";' to the ML session"
    31   echo
    32   echo "  INPUT (default \"$DEFAULT_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 COPYDB=""
    52 MLTEXT=""
    53 COPYDB=""
    54 MODES=""
    55 TERMINATE=""
    56 READONLY=""
    57 
    58 while getopts "ce:m:qru" OPT
    59 do
    60   case "$OPT" in
    61     c)
    62       COPYDB=true
    63       ;;
    64     e)
    65       MLTEXT="$MLTEXT $OPTARG"
    66       ;;
    67     m)
    68       if [ -z "$MODES" ]; then
    69         MODES="\"$OPTARG\""
    70       else
    71         MODES="\"$OPTARG\", $MODES"
    72       fi
    73       ;;
    74     q)
    75       TERMINATE=true
    76       ;;
    77     r)
    78       READONLY=true
    79       ;;
    80     u)
    81       MLTEXT="$MLTEXT exit_use_dir\".\";"
    82       ;;
    83     \?)
    84       usage
    85       ;;
    86   esac
    87 done
    88 
    89 shift $(($OPTIND - 1))
    90 
    91 
    92 # args
    93 
    94 INPUT=""
    95 OUTPUT=""
    96 
    97 if [ $# -ge 1 ]; then
    98   INPUT="$1"
    99   shift
   100 fi
   101 
   102 if [ $# -ge 1 ]; then
   103   OUTPUT="$1"
   104   shift
   105 fi
   106 
   107 [ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
   108 
   109 
   110 ## check ML system
   111 
   112 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   113 
   114 
   115 ## input heap file
   116 
   117 [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
   118 
   119 case "$INPUT" in
   120   RAW_ML_SYSTEM)
   121     INFILE=""
   122     ;;
   123   */*)
   124     INFILE="$INPUT"
   125     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   126     ;;
   127   *)
   128     ISA_PATH=""
   129     INFILE=""
   130     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   131     do
   132       ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"
   133       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   134     done
   135     if [ -z "$INFILE" ]; then
   136       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   137       for DIR in $ISA_PATH
   138       do
   139         echo "  $DIR" >&2
   140       done
   141       exit 2
   142     fi
   143     ;;
   144 esac
   145 
   146 
   147 ## output heap file
   148 
   149 case "$OUTPUT" in
   150   "")
   151     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   152     ;;
   153   */*)
   154     OUTFILE="$OUTPUT"
   155     ;;
   156   *)
   157     OUTDIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
   158     mkdir -p "$OUTDIR"
   159     OUTFILE="$OUTDIR/$OUTPUT"
   160     ;;
   161 esac
   162 
   163 
   164 ## run it!
   165 
   166 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   167 
   168 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   169 
   170 export INFILE OUTFILE COPYDB MLTEXT TERMINATE
   171 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   172 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE