equal
deleted
inserted
replaced
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 |