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