bin/isabelle
changeset 4333 1d326b826851
parent 3502 ec22ba0a26ec
child 4355 68c7c544570c
equal deleted inserted replaced
4332:d4a15e32c024 4333:1d326b826851
   153     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   153     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
   154     ;;
   154     ;;
   155 esac
   155 esac
   156 
   156 
   157 
   157 
       
   158 ## prepare tmp directory
       
   159 
       
   160 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
       
   161 
       
   162 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
       
   163 mkdir -p "$ISABELLE_TMP"
       
   164 
       
   165 
   158 ## run it!
   166 ## run it!
   159 
   167 
   160 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   168 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   161 
   169 
   162 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   170 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   163 
   171 
   164 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE
   172 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP
   165 [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
   173 
   166 exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
   174 if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
       
   175   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
       
   176 else
       
   177   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
       
   178 fi
       
   179 
       
   180 
       
   181 #Do not even think of 'rm -r'!!
       
   182 rmdir $ISABELLE_TMP