lib/Tools/usedir
changeset 11907 f2a5481c7998
parent 11847 82df5977101b
child 11949 38e20c036e37
equal deleted inserted replaced
11906:a71713885e3e 11907:f2a5481c7998
   186 
   186 
   187   OPT_C=""
   187   OPT_C=""
   188   [ "$COMPRESS" = true ] && OPT_C="-c"
   188   [ "$COMPRESS" = true ] && OPT_C="-c"
   189 
   189 
   190   "$ISABELLE" \
   190   "$ISABELLE" \
   191     -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
   191     -e "Session.use_dir true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
   192     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   192     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   193   RC="$?"
   193   RC="$?"
   194 else
   194 else
   195   ITEM=$(basename "$LOGIC")-"$SESSION"
   195   ITEM=$(basename "$LOGIC")-"$SESSION"
   196   echo "Running $ITEM ..." >&2
   196   echo "Running $ITEM ..." >&2
   197   LOG="$LOGDIR/$ITEM"
   197   LOG="$LOGDIR/$ITEM"
   198 
   198 
   199   "$ISABELLE" \
   199   "$ISABELLE" \
   200     -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
   200     -e "Session.use_dir false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
   201     -r -q "$LOGIC" > "$LOG"
   201     -r -q "$LOGIC" > "$LOG"
   202   RC="$?"
   202   RC="$?"
   203   cd ..
   203   cd ..
   204 fi
   204 fi
   205 
   205