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