eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
--- a/src/HOL/Mutabelle/etc/settings Fri Mar 25 17:09:21 2011 +0100
+++ b/src/HOL/Mutabelle/etc/settings Fri Mar 25 21:38:41 2011 +0100
@@ -4,6 +4,5 @@
MUTABELLE_LOGIC=HOL
MUTABELLE_IMPORT_THEORY=Complex_Main
-MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- 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