diff -r a51761c262d1 -r 21714b0de625 src/HOL/Mutabelle/lib/Tools/mutabelle --- a/src/HOL/Mutabelle/lib/Tools/mutabelle Fri Mar 25 17:09:21 2011 +0100 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Fri Mar 25 21:38:41 2011 +0100 @@ -8,6 +8,7 @@ PRG="$(basename "$0")" function usage() { + [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None" echo echo "Usage: isabelle $PRG [OPTIONS] THEORY" echo @@ -58,6 +59,11 @@ MUTABELLE_TEST_THEORY="$1" +if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then + MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$" + PURGE_OUTPUT="true" +fi + export MUTABELLE_OUTPUT_PATH @@ -121,3 +127,9 @@ echo "nitpick : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \ T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")" + +## cleanup + +if [ -n "$PURGE_OUTPUT" ]; then + rm -rf "$MUTABELLE_OUTPUT_PATH" +fi