bin/isabelle-process
changeset 17792 4a34fd6884b1
parent 16874 3057990d20e0
child 20923 059926d1d074
equal deleted inserted replaced
17791:f4453001cbde 17792:4a34fd6884b1
   151 case "$INPUT" in
   151 case "$INPUT" in
   152   RAW_ML_SYSTEM)
   152   RAW_ML_SYSTEM)
   153     INFILE=""
   153     INFILE=""
   154     ;;
   154     ;;
   155   */*)
   155   */*)
   156     INFILE="$INPUT"
   156     INFILE="$INPUT$ML_SUFFIX"
   157     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   157     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
   158     ;;
   158     ;;
   159   *)
   159   *)
   160     INFILE=""
   160     INFILE=""
   161     ISA_PATH=""
   161     ISA_PATH=""
   164     IFS=":"
   164     IFS=":"
   165     for DIR in $ISABELLE_PATH
   165     for DIR in $ISABELLE_PATH
   166     do
   166     do
   167       DIR="$DIR/$ML_IDENTIFIER"
   167       DIR="$DIR/$ML_IDENTIFIER"
   168       ISA_PATH="$ISA_PATH  $DIR\n"
   168       ISA_PATH="$ISA_PATH  $DIR\n"
   169       [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
   169       [ -z "$INFILE" -a -f "$DIR/$INPUT$ML_SUFFIX" ] && INFILE="$DIR/$INPUT$ML_SUFFIX"
   170     done
   170     done
   171     IFS="$ORIG_IFS"
   171     IFS="$ORIG_IFS"
   172 
   172 
   173     if [ -z "$INFILE" ]; then
   173     if [ -z "$INFILE" ]; then
   174       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   174       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
   184 case "$OUTPUT" in
   184 case "$OUTPUT" in
   185   "")
   185   "")
   186     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   186     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
   187     ;;
   187     ;;
   188   */*)
   188   */*)
   189     OUTFILE="$OUTPUT"
   189     OUTFILE="$OUTPUT$ML_SUFFIX"
   190     ;;
   190     ;;
   191   *)
   191   *)
   192     mkdir -p "$ISABELLE_OUTPUT"
   192     mkdir -p "$ISABELLE_OUTPUT"
   193     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   193     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT$ML_SUFFIX"
   194     ;;
   194     ;;
   195 esac
   195 esac
   196 
   196 
   197 
   197 
   198 ## prepare tmp directory
   198 ## prepare tmp directory
   199 
   199 
   200 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   200 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
   201 ISABELLE_PID="$$"
   201 ISABELLE_PID="$$"
   202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX${ISABELLE_PID}"
   202 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
   203 mkdir -p "$ISABELLE_TMP"
   203 mkdir -p "$ISABELLE_TMP"
   204 
   204 
   205 
   205 
   206 ## run it!
   206 ## run it!
   207 
   207