equal
deleted
inserted
replaced
212 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" |
212 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" |
213 |
213 |
214 NICE="nice" |
214 NICE="nice" |
215 if [ -n "$WRAPPER_OUTPUT" ]; then |
215 if [ -n "$WRAPPER_OUTPUT" ]; then |
216 [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT" |
216 [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT" |
217 MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";" |
217 MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";" |
218 elif [ -n "$PGIP" ]; then |
218 elif [ -n "$PGIP" ]; then |
219 MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;" |
219 MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;" |
220 elif [ -n "$PROOFGENERAL" ]; then |
220 elif [ -n "$PROOFGENERAL" ]; then |
221 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
221 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
222 elif [ "$ISAR" = true ]; then |
222 elif [ "$ISAR" = true ]; then |