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