bin/isabelle
changeset 2308 641be5ad47af
parent 2292 c1c5652600f1
child 2343 2588b63b42ca
equal deleted inserted replaced
2307:508d2a233dbc 2308:641be5ad47af
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
       
     3 # $Id$
       
     4 #
     3 # Basic Isabelle startup script.
     5 # Basic Isabelle startup script.
     4 #
       
     5 # $Id$
       
     6 
     6 
     7 
     7 
     8 ## settings
     8 ## settings
     9 
     9 
    10 ISABELLE_HOME=$(dirname $(dirname $0))
    10 ISABELLE_HOME=$(dirname $(dirname $0))
   108 [ $# -ne 0 ] && fail "Bad args: $*"
   108 [ $# -ne 0 ] && fail "Bad args: $*"
   109 
   109 
   110 
   110 
   111 ## check ML system
   111 ## check ML system
   112 
   112 
   113 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Sorry, no Isabelle."
   113 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
   114 
   114 
   115 
   115 
   116 ## input heap file
   116 ## input heap file
   117 
   117 
   118 [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
   118 [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
   124   */*)
   124   */*)
   125     INFILE="$INPUT"
   125     INFILE="$INPUT"
   126     [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
   126     [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
   127     ;;
   127     ;;
   128   *)
   128   *)
       
   129     ISA_PATH=""
   129     INFILE=""
   130     INFILE=""
   130     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   131     for DIR in $(echo $ISABELLE_PATH | tr : " ")
   131     do
   132     do
       
   133       ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"
   132       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   134       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
   133     done
   135     done
   134     [ -z "$INFILE" ] && fail "Unknown logic: \"$INPUT\""
   136     if [ -z "$INFILE" ]; then
       
   137       echo "Unknown logic \"$INPUT\" -- no heap file found in:"
       
   138       for DIR in $ISA_PATH
       
   139       do
       
   140         echo "  $DIR"
       
   141       done
       
   142       exit 2
       
   143     fi
   135     ;;
   144     ;;
   136 esac
   145 esac
   137 
   146 
   138 
   147 
   139 ## output heap file
   148 ## output heap file