src/HOL/Mutabelle/lib/Tools/mutabelle
changeset 42119 21714b0de625
parent 41949 f9a2e10c49cb
child 43148 092e38108f3f
--- 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