lib/Tools/usedir
changeset 48445 cb4136e4cabf
parent 42004 e06351ffb475
equal deleted inserted replaced
48444:c8c7b2b388d1 48445:cb4136e4cabf
   239   ITEM="$SESSION"
   239   ITEM="$SESSION"
   240   echo "Building $ITEM ..." >&2
   240   echo "Building $ITEM ..." >&2
   241   LOG="$LOGDIR/$ITEM"
   241   LOG="$LOGDIR/$ITEM"
   242 
   242 
   243   "$ISABELLE_PROCESS" \
   243   "$ISABELLE_PROCESS" \
   244     -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
   244     -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
   245     -q -w $LOGIC $NAME > "$LOG"
   245     -q -w $LOGIC $NAME > "$LOG"
   246   RC="$?"
   246   RC="$?"
   247 else
   247 else
   248   ITEM=$(basename "$LOGIC")-"$SESSION"
   248   ITEM=$(basename "$LOGIC")-"$SESSION"
   249   echo "Running $ITEM ..." >&2
   249   echo "Running $ITEM ..." >&2
   250   LOG="$LOGDIR/$ITEM"
   250   LOG="$LOGDIR/$ITEM"
   251 
   251 
   252   "$ISABELLE_PROCESS" \
   252   "$ISABELLE_PROCESS" \
   253     -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
   253     -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
   254     -r -q "$LOGIC" > "$LOG"
   254     -r -q "$LOGIC" > "$LOG"
   255   RC="$?"
   255   RC="$?"
   256   cd ..
   256   cd ..
   257 fi
   257 fi
   258 
   258